स्वचालित प्रमेय सिद्ध करना

From alpha
Jump to navigation Jump to search

स्वचालित प्रमेय सिद्ध करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) स्वचालित तर्क और गणितीय तर्क का एक उपक्षेत्र है जो कंप्यूटर प्रोग्राम द्वारा गणितीय प्रमेयों को सिद्ध करने से संबंधित है। गणितीय प्रमाण पर स्वचालित तर्क कंप्यूटर विज्ञान के विकास के लिए एक प्रमुख प्रेरणा थी।

तार्किक आधार

जबकि औपचारिक तर्कवाद की जड़ें अरिस्टोटेलियन तर्क तक जाती हैं, 19वीं सदी के अंत और 20वीं सदी की शुरुआत में आधुनिक तर्क और औपचारिक गणित का विकास हुआ। भगवान का शुक्र है फ्रीज के शब्द लेखन (1879) ने एक संपूर्ण प्रस्तावात्मक तर्क और अनिवार्य रूप से आधुनिक विधेय तर्क दोनों को प्रस्तुत किया।[1] 1884 में प्रकाशित उनकी अंकगणित की नींव,[2] गणित को औपचारिक तर्क में व्यक्त किया गया। इस दृष्टिकोण को बर्ट्रेंड रसेल और अल्फ्रेड नॉर्थ व्हाइटहेड ने अपने प्रभावशाली गणितीय सिद्धांत में जारी रखा, जो पहली बार 1910-1913 में प्रकाशित हुआ था।[3] और 1927 में संशोधित दूसरे संस्करण के साथ।[4] रसेल और व्हाइटहेड ने सोचा कि वे औपचारिक तर्क के सिद्धांतों और अनुमान नियमों का उपयोग करके सभी गणितीय सत्य प्राप्त कर सकते हैं, सिद्धांत रूप में प्रक्रिया को स्वचालितकरण के लिए खोल सकते हैं। 1920 में, थोरल्फ़ स्कोलेम ने लियोपोल्ड लोवेनहेम द्वारा पिछले परिणाम को सरल बनाया, जिससे लोवेनहेम-स्कोलेम प्रमेय और 1930 में, एक हेरब्रांड ब्रह्मांड और एक हेरब्रांड व्याख्या की धारणा बनी, जिसने प्रथम-क्रम सूत्रों (और इसलिए एक प्रमेय की वैधता (तर्क)) की संतुष्टि को (संभावित रूप से असीम रूप से कई) प्रस्तावात्मक संतुष्टि समस्याओं में कम करने की अनुमति दी।[5] 1929 में, मोजेज़ प्रेस्बर्गर ने दिखाया कि जोड़ और समानता के साथ प्राकृतिक संख्याओं का सिद्धांत (जिसे अब उनके सम्मान में प्रेस्बर्गर अंकगणित कहा जाता है) निर्णायकता (तर्क) है और एक एल्गोरिदम दिया जो यह निर्धारित कर सकता है कि भाषा में दिया गया वाक्य सही था या गलत।[6][7] हालाँकि, इस सकारात्मक परिणाम के तुरंत बाद, कर्ट गोडेल ने प्रिंसिपिया मैथमेटिका और संबंधित सिस्टम (1931) के औपचारिक रूप से अनिर्णीत प्रस्तावों पर प्रकाशित किया, जिसमें दिखाया गया कि किसी भी पर्याप्त रूप से मजबूत स्वयंसिद्ध प्रणाली में सच्चे कथन होते हैं जिन्हें सिस्टम में साबित नहीं किया जा सकता है। इस विषय को 1930 के दशक में अलोंजो चर्च और एलन ट्यूरिंग द्वारा आगे विकसित किया गया था, जिन्होंने एक ओर कम्प्यूटेबिलिटी की दो स्वतंत्र लेकिन समकक्ष परिभाषाएँ दीं, और दूसरी ओर अनिर्णीत प्रश्नों के लिए ठोस उदाहरण दिए।

पहला कार्यान्वयन

द्वितीय विश्व युद्ध के तुरंत बाद, पहला सामान्य प्रयोजन कंप्यूटर उपलब्ध हो गया। 1954 में, मार्टिन डेविस (गणितज्ञ) ने प्रिंसटन, न्यू जर्सी में उन्नत अध्ययन संस्थान में जॉन्नियाक वैक्यूम ट्यूब कंप्यूटर के लिए प्रेस्बर्गर के एल्गोरिदम को प्रोग्राम किया। डेविस के अनुसार, इसकी महान विजय यह सिद्ध करना था कि दो सम संख्याओं का योग भी सम होता है।[7][8] 1956 में तर्क सिद्धांत मशीन अधिक महत्वाकांक्षी थी, जो एलन नेवेल, हर्बर्ट ए. साइमन और क्लिफ शॉ|जे द्वारा विकसित प्रिंसिपिया मैथमेटिका के प्रस्तावित तर्क के लिए एक कटौती प्रणाली थी। सी. शॉ. साथ ही जॉन्नियाक पर चलते हुए, लॉजिक थ्योरी मशीन ने प्रस्तावात्मक सिद्धांतों और तीन कटौती नियमों के एक छोटे सेट से प्रमाण तैयार किए: मूड सेट करना , (प्रस्तावात्मक) परिवर्तनीय प्रतिस्थापन, और उनकी परिभाषा के अनुसार सूत्रों का प्रतिस्थापन। प्रणाली ने अनुमानी मार्गदर्शन का उपयोग किया, और प्रिंसिपिया के पहले 52 प्रमेयों में से 38 को सिद्ध करने में कामयाब रही।[7]

लॉजिक थ्योरी मशीन के अनुमानी दृष्टिकोण ने मानव गणितज्ञों का अनुकरण करने की कोशिश की, और यह गारंटी नहीं दे सका कि सैद्धांतिक रूप से भी हर वैध प्रमेय के लिए एक प्रमाण पाया जा सकता है। इसके विपरीत, अन्य, अधिक व्यवस्थित एल्गोरिदम ने, कम से कम सैद्धांतिक रूप से, प्रथम-क्रम तर्क के लिए पूर्णता (तर्क) हासिल की। प्रारंभिक दृष्टिकोण हेरब्रांड ब्रह्मांड के शब्दों के साथ चर को त्वरित करके पहले क्रम के सूत्र को प्रस्ताव सूत्रों के क्रमिक रूप से बड़े सेट में परिवर्तित करने के लिए हेरब्रांड और स्कोलेम के परिणामों पर निर्भर थे। फिर कई तरीकों का उपयोग करके प्रस्ताव सूत्रों को असंतोषजनकता के लिए जांचा जा सकता है। गिलमोर के कार्यक्रम में विच्छेदनात्मक सामान्य रूप में रूपांतरण का उपयोग किया गया, एक ऐसा रूप जिसमें किसी सूत्र की संतुष्टि स्पष्ट होती है।[7][9]


समस्या की निर्णायकता

अंतर्निहित तर्क के आधार पर, किसी सूत्र की वैधता तय करने की समस्या तुच्छ से असंभव तक भिन्न होती है। प्रस्तावात्मक तर्क के लगातार मामले के लिए, समस्या निर्णय योग्य है लेकिन सह-एनपी-पूर्ण है, और इसलिए सामान्य प्रमाण कार्यों के लिए केवल घातांक-समय एल्गोरिदम मौजूद माना जाता है। प्रथम-क्रम तर्क के लिए, गोडेल की पूर्णता प्रमेय में कहा गया है कि प्रमेय (सिद्ध करने योग्य कथन) बिल्कुल तार्किक रूप से मान्य सुगठित सूत्र हैं, इसलिए वैध सूत्रों की पहचान करना पुनरावर्ती रूप से गणना योग्य है: असीमित संसाधनों को देखते हुए, किसी भी वैध सूत्र को अंततः सिद्ध किया जा सकता है। हालाँकि, अमान्य सूत्र (वे जो किसी दिए गए सिद्धांत में शामिल नहीं हैं) को हमेशा पहचाना नहीं जा सकता है।

उपरोक्त पहले क्रम के सिद्धांतों पर लागू होता है, जैसे कि पीनो अभिगृहीत हालाँकि, किसी विशिष्ट मॉडल के लिए जिसे प्रथम क्रम सिद्धांत द्वारा वर्णित किया जा सकता है, कुछ कथन सत्य हो सकते हैं लेकिन मॉडल का वर्णन करने के लिए उपयोग किए जाने वाले सिद्धांत में अनिर्णीत हो सकते हैं। उदाहरण के लिए, गोडेल की अपूर्णता प्रमेय से, हम जानते हैं कि कोई भी सिद्धांत जिसके उचित स्वयंसिद्ध प्राकृतिक संख्याओं के लिए सत्य हैं, सभी प्रथम क्रम के कथनों को प्राकृतिक संख्याओं के लिए सत्य साबित नहीं कर सकता है, भले ही उचित स्वयंसिद्धों की सूची को अनंत गणना योग्य होने की अनुमति दी गई हो। इसका तात्पर्य यह है कि एक स्वचालित प्रमेय कहावत प्रमाण की खोज करते समय समाप्त होने में विफल हो जाएगी, जब जांच की जा रही कथन उपयोग किए जा रहे सिद्धांत में अनिर्णीत हो, भले ही वह रुचि के मॉडल में सत्य हो। इस सैद्धांतिक सीमा के बावजूद, व्यवहार में, प्रमेय सिद्धकर्ता कई कठिन समस्याओं को हल कर सकते हैं, यहां तक ​​कि उन मॉडलों में भी जो किसी भी प्रथम क्रम सिद्धांत (जैसे पूर्णांक) द्वारा पूरी तरह से वर्णित नहीं हैं।

संबंधित समस्याएँ

एक सरल, लेकिन संबंधित, समस्या प्रमाण सत्यापन है, जहां एक प्रमेय के लिए मौजूदा प्रमाण को वैध प्रमाणित किया जाता है। इसके लिए, आम तौर पर यह आवश्यक है कि प्रत्येक व्यक्तिगत प्रमाण चरण को एक आदिम पुनरावर्ती फ़ंक्शन या प्रोग्राम द्वारा सत्यापित किया जा सके, और इसलिए समस्या हमेशा निर्णय योग्य होती है।

चूंकि स्वचालित प्रमेय प्रोवर्स द्वारा उत्पन्न प्रमाण आम तौर पर बहुत बड़े होते हैं, इसलिए प्रूफ संपीड़न की समस्या महत्वपूर्ण है और प्रोवर के आउटपुट को छोटा बनाने के उद्देश्य से विभिन्न तकनीकों का विकास किया गया है, और परिणामस्वरूप अधिक आसानी से समझने योग्य और जांचने योग्य बनाया गया है।

प्रूफ सहायकों को सिस्टम को संकेत देने के लिए एक मानव उपयोगकर्ता की आवश्यकता होती है। स्वचालन की डिग्री के आधार पर, प्रूवर को अनिवार्य रूप से एक प्रूफ चेकर में तब्दील किया जा सकता है, जिसमें उपयोगकर्ता औपचारिक तरीके से सबूत संपीड़न करता है, या महत्वपूर्ण प्रूफ कार्य स्वचालित रूप से किए जा सकते हैं। इंटरएक्टिव प्रोवर्स का उपयोग विभिन्न प्रकार के कार्यों के लिए किया जाता है, लेकिन यहां तक ​​कि पूरी तरह से स्वचालित सिस्टम ने भी कई दिलचस्प और कठिन प्रमेय साबित किए हैं, जिनमें कम से कम एक प्रमेय भी शामिल है जो लंबे समय से मानव गणितज्ञों से दूर रहा है, अर्थात् रॉबिन्स अनुमान।[10][11] हालाँकि, ये सफलताएँ छिटपुट होती हैं, और कठिन समस्याओं पर काम करने के लिए आमतौर पर एक कुशल उपयोगकर्ता की आवश्यकता होती है।

कभी-कभी प्रमेय सिद्ध करने और अन्य तकनीकों के बीच एक और अंतर खींचा जाता है, जहां एक प्रक्रिया को प्रमेय सिद्ध माना जाता है यदि इसमें एक पारंपरिक प्रमाण शामिल होता है, जो सिद्धांतों से शुरू होता है और अनुमान के नियमों का उपयोग करके नए अनुमान चरणों का उत्पादन करता है। अन्य तकनीकों में मॉडल जाँच शामिल होगी, जिसमें, सबसे सरल मामले में, कई संभावित राज्यों की क्रूर-बल गणना शामिल है (हालांकि मॉडल चेकर्स के वास्तविक कार्यान्वयन के लिए बहुत चतुराई की आवश्यकता होती है, और यह केवल क्रूर बल तक ही सीमित नहीं है)।

हाइब्रिड प्रमेय साबित करने वाली प्रणालियाँ हैं जो मॉडल जाँच को एक अनुमान नियम के रूप में उपयोग करती हैं। ऐसे कार्यक्रम भी हैं जो किसी विशेष प्रमेय को सिद्ध करने के लिए लिखे गए थे, (आमतौर पर अनौपचारिक) प्रमाण के साथ कि यदि कार्यक्रम एक निश्चित परिणाम के साथ समाप्त होता है, तो प्रमेय सत्य है। इसका एक अच्छा उदाहरण चार रंग प्रमेय का मशीन-सहायता प्राप्त प्रमाण था, जो पहले दावा किए गए गणितीय प्रमाण के रूप में बहुत विवादास्पद था, जिसे कार्यक्रम की गणना के विशाल आकार के कारण मनुष्यों द्वारा सत्यापित करना अनिवार्य रूप से असंभव था (ऐसे प्रमाणों को गैर-सर्वेक्षण योग्य प्रमाण कहा जाता है)। प्रोग्राम-असिस्टेड प्रूफ का एक और उदाहरण वह है जो दर्शाता है कि चार कनेक्ट करें का गेम हमेशा पहला खिलाड़ी ही जीत सकता है।

औद्योगिक उपयोग

स्वचालित प्रमेय सिद्ध करने का व्यावसायिक उपयोग ज्यादातर एकीकृत सर्किट डिजाइन और सत्यापन में केंद्रित है। पेंटियम FDIV बग के बाद से, आधुनिक माइक्रोप्रोसेसरों की जटिल फ़्लोटिंग पॉइंट इकाई को अतिरिक्त जांच के साथ डिजाइन किया गया है। एएमडी, इंटेल और अन्य स्वचालित प्रमेय का उपयोग करते हैं जो यह सत्यापित करते हैं कि उनके प्रोसेसर में विभाजन और अन्य संचालन सही ढंग से लागू किए गए हैं।

प्रथम-क्रम प्रमेय सिद्ध करना

1960 के दशक के उत्तरार्ध में स्वचालित कटौती में अनुसंधान को वित्तपोषित करने वाली एजेंसियों ने व्यावहारिक अनुप्रयोगों की आवश्यकता पर जोर देना शुरू कर दिया। पहले उपयोगी क्षेत्रों में से एक प्रोग्राम सत्यापन था, जिसके तहत पास्कल, एडा आदि भाषाओं में कंप्यूटर प्रोग्रामों की शुद्धता को सत्यापित करने की समस्या के लिए प्रथम-क्रम प्रमेय प्रूवर्स को लागू किया गया था। प्रारंभिक प्रोग्राम सत्यापन प्रणालियों में उल्लेखनीय स्टैनफोर्ड पास्कल सत्यापनकर्ता था। स्टैनफोर्ड विश्वविद्यालय में डेविड लक्खम द्वारा विकसित।[12][13][14] यह स्टैनफोर्ड रेजोल्यूशन प्रोवर पर आधारित था जिसे जॉन एलन रॉबिन्सन के संकल्प (तर्क)तर्क) सिद्धांत का उपयोग करके स्टैनफोर्ड में भी विकसित किया गया था। गणितीय समस्याओं को हल करने की क्षमता प्रदर्शित करने वाली यह पहली स्वचालित कटौती प्रणाली थी, जिसकी घोषणा औपचारिक रूप से समाधान प्रकाशित होने से पहले अमेरिकन गणितीय सोसायटी के नोटिस में की गई थी।[citation needed]

प्रथम-क्रम तर्क|प्रथम-क्रम प्रमेय सिद्ध करना स्वचालित प्रमेय सिद्ध करने के सबसे परिपक्व उपक्षेत्रों में से एक है। तर्क इतना अभिव्यंजक है कि मनमाने ढंग से समस्याओं के विनिर्देशन की अनुमति देता है, अक्सर उचित प्राकृतिक और सहज तरीके से। दूसरी ओर, यह अभी भी अर्ध-निर्णय योग्य है, और पूरी तरह से स्वचालित प्रणालियों को सक्षम करते हुए कई ध्वनि और पूर्ण गणना विकसित की गई हैं।[15] अधिक अभिव्यंजक तर्क, जैसे कि उच्च-क्रम तर्क, प्रथम-क्रम तर्क की तुलना में समस्याओं की एक विस्तृत श्रृंखला की सुविधाजनक अभिव्यक्ति की अनुमति देते हैं, लेकिन इन तर्कों के लिए सिद्ध करने वाला प्रमेय कम विकसित है।[16][17]


मानदंड, प्रतियोगिताएं, और स्रोत

कार्यान्वित प्रणालियों की गुणवत्ता को मानक बेंचमार्क उदाहरणों की एक बड़ी लाइब्रेरी के अस्तित्व से लाभ हुआ है - थ्योरम प्रोवर्स के लिए हजारों समस्याएं (टीपीटीपी) समस्या लाइब्रेरी[18] - साथ ही सीएडीई एटीपी सिस्टम प्रतियोगिता (सीएएससी) से, जो प्रथम-क्रम समस्याओं के कई महत्वपूर्ण वर्गों के लिए प्रथम-क्रम प्रणालियों की एक वार्षिक प्रतियोगिता है।

कुछ महत्वपूर्ण प्रणालियाँ (सभी ने कम से कम एक CASC प्रतियोगिता प्रभाग जीता है) नीचे सूचीबद्ध हैं।

  • ई प्रमेय कहावत पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन कहावत है, लेकिन एक सुपरपोजिशन कैलकुलस पर निर्मित है, जिसे मूल रूप से वोल्फगैंग बाइबिल के निर्देशन में म्यूनिख के तकनीकी विश्वविद्यालय के स्वचालित तर्क समूह में विकसित किया गया है, और अब बाडेन-वुर्टेमबर्ग सहकारी में विकसित किया गया है। स्टटगर्ट में राज्य विश्वविद्यालय.
  • आर्गोन नेशनल लेबोरेटरी में विकसित ओटर (प्रमेय कहावत), प्रथम-क्रम रिज़ॉल्यूशन और पैरामॉड्यूलेशन पर आधारित है। तब से ओटर को Prover9 द्वारा प्रतिस्थापित कर दिया गया है, जिसे Mace4 के साथ जोड़ा गया है।
  • SETHEO लक्ष्य-निर्देशित मॉडल उन्मूलन कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय सिद्धr E-SETHEO में E और SETHEO को (अन्य प्रणालियों के साथ) संयोजित किया गया है।
  • वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोनकोव और क्रिस्टोफ़ होडर द्वारा मैनचेस्टर विश्वविद्यालय में विकसित और कार्यान्वित की गई थी। इसे अब एक बढ़ती हुई अंतर्राष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है।
  • वाल्डमिस्टर इकाई-समीकरण प्रथम-क्रम तर्क के लिए अर्निम बुच और थॉमस हिलेंब्रांड द्वारा विकसित एक विशेष प्रणाली है। इसने लगातार चौदह वर्षों (1997-2010) तक सीएएससी यूईक्यू डिवीजन जीता।
  • SPASS समानता के साथ प्रथम क्रम तर्क प्रमेय कहावत है। इसे कंप्यूटर विज्ञान के लिए मैक्स प्लैंक संस्थान के अनुसंधान समूह ऑटोमेशन ऑफ लॉजिक द्वारा विकसित किया गया है।

प्रमेय कहावत संग्रहालय[19] भविष्य के विश्लेषण के लिए प्रमेय कहावत प्रणालियों के स्रोतों को संरक्षित करने की एक पहल है, क्योंकि वे महत्वपूर्ण सांस्कृतिक/वैज्ञानिक कलाकृतियाँ हैं। इसमें ऊपर उल्लिखित कई प्रणालियों के स्रोत हैं।

लोकप्रिय तकनीक


सॉफ्टवेयर सिस्टम

See also: Proof assistant § Comparison, and Category:Theorem proving software systems
Comparison
Name License type Web service Library Standalone Last update (YYYY-mm-dd format)
ACL2 3-clause BSD No No Yes May 2019
Prover9/Otter Public Domain Via System on TPTP Yes No 2009
Jape GPLv2 Yes Yes No May 15, 2015
PVS GPLv2 No Yes No January 14, 2013
EQP ? No Yes No May 2009
PhoX ? No Yes No September 28, 2017
E GPL Via System on TPTP No Yes July 4, 2017
SNARK Mozilla Public License 1.1 No Yes No 2012
Vampire Vampire License Via System on TPTP Yes Yes December 14, 2017
Theorem Proving System (TPS) TPS Distribution Agreement No Yes No February 4, 2012
SPASS FreeBSD license Yes Yes Yes November 2005
IsaPlanner GPL No Yes Yes 2007
KeY GPL Yes Yes Yes October 11, 2017
Z3 Theorem Prover MIT License Yes Yes Yes November 19, 2019


मुफ्त सॉफ्टवेयर

मालिकाना सॉफ्टवेयर

यह भी देखें

टिप्पणियाँ

  1. ↑ Frege, Gottlob (1879). शब्द लेखन. Verlag Louis Neuert.
  2. ↑ Frege, Gottlob (1884). अंकगणित की मूल बातें (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02.
  3. ↑ Bertrand Russell; Alfred North Whitehead (1910–1913). गणितीय सिद्धांत (1st ed.). Cambridge University Press.
  4. ↑ Bertrand Russell; Alfred North Whitehead (1927). गणितीय सिद्धांत (2nd ed.). Cambridge University Press.
  5. ↑ Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD). University of Paris.
  6. ↑ Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
  7. ↑ 7.0 7.1 7.2 7.3 Davis, Martin (2001). "The Early History of Automated Deduction". Robinson & Voronkov 2001.)
  8. ↑ Bibel, Wolfgang (2007). "स्वचालित कटौती का प्रारंभिक इतिहास और परिप्रेक्ष्य" (PDF). Ki 2007. LNAI. Springer (4667): 2–18. Archived (PDF) from the original on 2022-10-09. Retrieved 2 September 2012.
  9. ↑ Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation". IBM Journal of Research and Development. 4: 28–35. doi:10.1147/rd.41.0028.
  10. ↑ McCune, W.W. (1997). "रॉबिन्स समस्या का समाधान". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881. S2CID 30847540.
  11. ↑ Gina Kolata (December 10, 1996). "कंप्यूटर गणित प्रमाण तर्क शक्ति को दर्शाता है". The New York Times. Retrieved 2008-10-11.
  12. ↑ David C. Luckham and Norihisa Suzuki (Mar 1976). Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers (Technical Report AD-A027 455). Defense Technical Information Center. Archived from the original on August 12, 2021.
  13. ↑ Luckham, David C.; Suzuki, Norihisa (Oct 1979). "पास्कल में ऐरे, रिकॉर्ड और पॉइंटर ऑपरेशंस का सत्यापन". ACM Transactions on Programming Languages and Systems. 1 (2): 226–244. doi:10.1145/357073.357078. S2CID 10088183.
  14. ↑ Luckham, D.; German, S.; von Henke, F.; Karp, R.; Milne, P.; Oppen, D.; Polak, W.; Scherlis, W. (1979). स्टैनफोर्ड पास्कल सत्यापनकर्ता उपयोगकर्ता मैनुअल (Technical report). Stanford University. CS-TR-79-731.
  15. ↑ Loveland, D W (1986). "Automated theorem proving: mapping logic into AI". Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems. Knoxville, Tennessee, United States: ACM Press: 224. doi:10.1145/12808.12833. ISBN 978-0-89791-206-8. S2CID 14361631.
  16. ↑ Kerber, Manfred. "How to prove higher order theorems in first order logic." (1999).
  17. ↑ Benzmüller, Christoph, et al. "LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2008.
  18. ↑ Sutcliffe, Geoff. "स्वचालित प्रमेय सिद्ध करने के लिए टीपीटीपी समस्या लाइब्रेरी". Retrieved 15 July 2019.
  19. ↑ "प्रमेय कहावत संग्रहालय". Michael Kohlhase. Retrieved 2022-11-20.
  20. ↑ Bundy, Alan (1999). गणितीय प्रेरण द्वारा प्रमाण का स्वचालन (PDF) (Technical report). Informatics Research Report. Vol. 2. Division of Informatics, University of Edinburgh. hdl:1842/3394.
  21. ↑ Gabbay, Dov M., and Hans Jürgen Ohlbach. "Quantifier elimination in second-order predicate logic." (1992).


संदर्भ


बाहरी संबंध

Retrieved from "https://alpha.indicwiki.in/index.php?title=स्वचालित_प्रमेय_सिद्ध_करना&oldid=259785"