स्वचालित प्रमेय प्रमाणन: Difference between revisions

From Vigyanwiki
No edit summary
Line 1: Line 1:
{{short description|Subfield of automated reasoning and mathematical logic}}
{{short description|Subfield of automated reasoning and mathematical logic}}
स्वचालित प्रमेय साबित करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) [[स्वचालित तर्क]] और [[गणितीय तर्क]] का एक उपक्षेत्र है जो [[कंप्यूटर प्रोग्राम]] द्वारा [[गणितीय प्रमेय]]ों को साबित करने से संबंधित है। [[गणितीय प्रमाण]] पर स्वचालित तर्क [[कंप्यूटर विज्ञान]] के विकास के लिए एक प्रमुख प्रेरणा थी।
स्वचालित प्रमेय प्रमाणित करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) [[स्वचालित तर्क]] एवं [[गणितीय तर्क]] का उपक्षेत्र है जो [[कंप्यूटर प्रोग्राम]] द्वारा [[गणितीय प्रमेय]] को प्रमाणित करने से संबंधित है। [[गणितीय प्रमाण]] पर स्वचालित तर्क [[कंप्यूटर विज्ञान]] के विकास के लिए प्रमुख प्रेरणा थी।


== तार्किक नींव ==
== तार्किक नींव ==
जबकि औपचारिक [[तर्कवाद]] की जड़ें [[अरिस्टोटेलियन तर्क]] में वापस जाती हैं, 19वीं सदी के अंत और 20वीं सदी की शुरुआत में आधुनिक तर्कशास्त्र और औपचारिक गणित का विकास हुआ। गॉटलॉब फ्रेगे के [[शब्द लेखन]] (1879) ने एक पूर्ण प्रस्तावात्[[मक तर्क]] और अनिवार्य रूप से आधुनिक [[विधेय तर्क]] दोनों का परिचय दिया।<ref>{{cite book|last=Frege|first=Gottlob|title=शब्द लेखन|year=1879|publisher=Verlag Louis Neuert|url=http://gallica.bnf.fr/ark:/12148/bpt6k65658c}}</ref> उनकी [[अंकगणित की नींव]], 1884 में प्रकाशित,<ref>{{cite book|last=Frege|first=Gottlob|title=अंकगणित की मूल बातें|year=1884|publisher=Wilhelm Kobner|location=Breslau|url=http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|access-date=2012-09-02|archive-url=https://web.archive.org/web/20070926172317/http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|archive-date=2007-09-26|url-status=dead}}</ref> औपचारिक तर्क में व्यक्त (के भाग) गणित। इस दृष्टिकोण को [[बर्ट्रेंड रसेल]] और [[अल्फ्रेड नॉर्थ व्हाइटहेड]] ने अपने प्रभावशाली [[ गणितीय सिद्धांत ]] में जारी रखा, जो पहली बार 1910-1913 में प्रकाशित हुआ था।<ref>{{cite book|title=गणितीय सिद्धांत|url=https://archive.org/details/cu31924001575244|year=1910–1913|publisher=Cambridge University Press|author=Bertrand Russell|edition=1st|author2=Alfred North Whitehead}}</ref> और 1927 में एक संशोधित दूसरे संस्करण के साथ।<ref>{{cite book|title=गणितीय सिद्धांत|url=https://archive.org/details/in.ernet.dli.2015.221192|year=1927|publisher=Cambridge University Press|author=Bertrand Russell|edition=2nd|author2=Alfred North Whitehead}}</ref> रसेल और व्हाइटहेड ने सोचा कि वे औपचारिक तर्क के सिद्धांतों और अनुमान नियमों का उपयोग करके सभी गणितीय सत्य प्राप्त कर सकते हैं, सैद्धांतिक रूप से प्रक्रिया को स्वचालित करने के लिए खोल सकते हैं। 1920 में, [[थोराल्फ़ स्कोलेम]] ने लियोपोल्ड लोवेनहेम द्वारा पिछले परिणाम को सरल बनाया, जिससे लोवेनहेम-स्कोलेम प्रमेय और 1930 में, एक हेरब्रांड ब्रह्मांड की धारणा और एक हेरब्रांड व्याख्या की अनुमति मिली (अ) प्रथम-क्रम के सूत्रों की संतुष्टि (और इसलिए) एक प्रमेय की [[वैधता (तर्क)]]) को कम करने के लिए (संभावित असीम रूप से कई) प्रस्तावनात्मक संतुष्टि की समस्याएं।<ref>{{cite thesis |first=J. |last=Herbrand |title=Recherches sur la théorie de la démonstration |date=1930 |type=PhD |publisher=University of Paris |url=https://eudml.org/doc/192791}}</ref>
जबकि औपचारिक [[तर्कवाद]] की जड़ें [[अरिस्टोटेलियन तर्क]] में वापस जाती हैं, 19वीं सदी के अंत एवं 20वीं सदी की प्रारम्भ में आधुनिक तर्कशास्त्र एवं औपचारिक गणित का विकास हुआ। गॉटलॉब फ्रेगे के [[शब्द लेखन]] (1879) ने पूर्ण [[मक तर्क|प्रस्तावात्मक तर्क]] एवं अनिवार्य रूप से आधुनिक [[विधेय तर्क]] दोनों का परिचय दिया।<ref>{{cite book|last=Frege|first=Gottlob|title=शब्द लेखन|year=1879|publisher=Verlag Louis Neuert|url=http://gallica.bnf.fr/ark:/12148/bpt6k65658c}}</ref> उनकी [[अंकगणित की नींव]], 1884 में प्रकाशित,<ref>{{cite book|last=Frege|first=Gottlob|title=अंकगणित की मूल बातें|year=1884|publisher=Wilhelm Kobner|location=Breslau|url=http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|access-date=2012-09-02|archive-url=https://web.archive.org/web/20070926172317/http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|archive-date=2007-09-26|url-status=dead}}</ref> औपचारिक तर्क में व्यक्त (के भाग) गणित इस दृष्टिकोण को [[बर्ट्रेंड रसेल]] एवं [[अल्फ्रेड नॉर्थ व्हाइटहेड]] ने अपने प्रभावशाली [[ गणितीय सिद्धांत ]] में निर्धारित रखा, जो प्रथम बार 1910-1913 में प्रकाशित हुआ था।<ref>{{cite book|title=गणितीय सिद्धांत|url=https://archive.org/details/cu31924001575244|year=1910–1913|publisher=Cambridge University Press|author=Bertrand Russell|edition=1st|author2=Alfred North Whitehead}}</ref> एवं 1927 में एक संशोधित दूसरे संस्करण के साथ<ref>{{cite book|title=गणितीय सिद्धांत|url=https://archive.org/details/in.ernet.dli.2015.221192|year=1927|publisher=Cambridge University Press|author=Bertrand Russell|edition=2nd|author2=Alfred North Whitehead}}</ref> रसेल एवं व्हाइटहेड ने सोचा कि वे औपचारिक तर्क के सिद्धांतों एवं अनुमान नियमों का उपयोग करके सभी गणितीय सत्य प्राप्त कर सकते हैं, सैद्धांतिक रूप से प्रक्रिया को स्वचालित करने के लिए विवृत कर सकते हैं। 1920 में, [[थोराल्फ़ स्कोलेम]] ने लियोपोल्ड लोवेनहेम द्वारा पूर्व परिणाम को सरल बनाया, जिससे लोवेनहेम-स्कोलेम प्रमेय एवं 1930 में, हेरब्रांड ब्रह्मांड की धारणा एवं हेरब्रांड व्याख्या की अनुमति मिली (अ) प्रथम-क्रम के सूत्रों की संतुष्टि (एवं इसलिए) प्रमेय की [[वैधता (तर्क)]]) को अर्घ्य करने के लिए (संभावित असीम रूप से कई) प्रस्तावनात्मक संतुष्टि की समस्याएं <ref>{{cite thesis |first=J. |last=Herbrand |title=Recherches sur la théorie de la démonstration |date=1930 |type=PhD |publisher=University of Paris |url=https://eudml.org/doc/192791}}</ref> 1929 में, मोजेज प्रेस्बर्गर ने दिखाया कि जोड़ एवं समानता के साथ [[प्राकृतिक संख्या]]ओं का सिद्धांत (अब उनके सम्मान में प्रेस्बर्गर अंकगणित कहा जाता है) निर्णायकता (तर्क) है एवं एल्गोरिथ्म दिया जो, यह निर्धारित कर सकता है कि भाषा में दिया गया वाक्य सही था या गलत,<ref>{{cite journal|last=Presburger|first=Mojżesz|title=Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt|journal=Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves|year=1929|pages=92–101|location=Warszawa}}</ref><ref name=Davis2001>{{Cite book
1929 में, Mojżesz Presburger ने दिखाया कि जोड़ और समानता के साथ [[प्राकृतिक संख्या]]ओं का सिद्धांत (अब उनके सम्मान में Presburger अंकगणित कहा जाता है) Decidability (तर्क) है और एक एल्गोरिथ्म दिया जो यह निर्धारित कर सकता है कि भाषा में दिया गया वाक्य सही था या गलत।<ref>{{cite journal|last=Presburger|first=Mojżesz|title=Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt|journal=Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves|year=1929|pages=92–101|location=Warszawa}}</ref><ref name=Davis2001>{{Cite book
| last = Davis
| last = Davis
| first = Martin
| first = Martin
Line 12: Line 11:
| chapter-url = http://cs.nyu.edu/cs/faculty/davism/early.ps
| chapter-url = http://cs.nyu.edu/cs/faculty/davism/early.ps
| title = {{harvnb|Robinson|Voronkov|2001}}
| title = {{harvnb|Robinson|Voronkov|2001}}
}})</ref>
}})</ref> चूंकि, इस सकारात्मक परिणाम के तुरंत पश्चात, कर्ट गोडेल ने प्रिन्सिपिया मैथेमेटिका एवं संबंधित प्रणालियों (1931) के औपचारिक रूप से अनिर्णायक प्रस्तावों पर प्रकाशित किया, यह दर्शाता है कि किसी भी पर्याप्त रूप से ठोस स्वयं सिद्ध प्रणाली में सत्य कथन होते हैं जिन्हें प्रणाली में सिद्ध नहीं किया जा सकता है। 1930 के दशक में [[अलोंजो चर्च]] एवं [[एलन ट्यूरिंग]] द्वारा इस विषय को विकसित किया गया, जिन्होंने [[कम्प्यूटेबिलिटी]] की दो स्वतंत्र किन्तु समकक्ष परिभाषाएं दीं, एवं दूसरी ओर अनिर्णीत प्रश्नों के लिए ठोस उदाहरण दिए है।
हालांकि, इस सकारात्मक परिणाम के तुरंत बाद, कर्ट गोडेल ने प्रिन्सिपिया मैथेमेटिका और संबंधित प्रणालियों (1931) के औपचारिक रूप से अनिर्णायक प्रस्तावों पर प्रकाशित किया, यह दर्शाता है कि किसी भी पर्याप्त रूप से मजबूत स्वयंसिद्ध प्रणाली में सच्चे कथन होते हैं जिन्हें प्रणाली में सिद्ध नहीं किया जा सकता है। 1930 के दशक में [[अलोंजो चर्च]] और [[एलन ट्यूरिंग]] द्वारा इस विषय को और विकसित किया गया, जिन्होंने एक ओर [[कम्प्यूटेबिलिटी]] की दो स्वतंत्र लेकिन समकक्ष परिभाषाएं दीं, और दूसरी ओर अनिर्णीत प्रश्नों के लिए ठोस उदाहरण दिए।


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


[[द्वितीय विश्व युद्ध]] के फौरन बाद, पहले सामान्य प्रयोजन के कंप्यूटर उपलब्ध हो गए। 1954 में, [[मार्टिन डेविस (गणितज्ञ)]] ने प्रिंसटन, न्यू जर्सी में [[उन्नत अध्ययन संस्थान]] में [[JOHNNIAC]] वैक्यूम ट्यूब कंप्यूटर के लिए प्रेस्बर्गर के एल्गोरिदम को प्रोग्राम किया। डेविस के अनुसार इसकी महान विजय यह सिद्ध करना था कि दो सम संख्याओं का योग सम होता है।<ref name=Davis2001/><ref name=Bibel2007>{{cite journal|last=Bibel|first=Wolfgang|title=प्रारंभिक इतिहास और स्वचालित कटौती के परिप्रेक्ष्य|journal=Ki 2007|year=2007|series=LNAI|issue=4667|pages=2–18|url=http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-date=2022-10-09 |url-status=live|access-date=2 September 2012|publisher=Springer}}</ref> 1956 में [[ तर्क सिद्धांत मशीन ]] अधिक महत्वाकांक्षी थी, [[ एलन नेवेल ]], हर्बर्ट ए. साइमन और क्लिफ शॉ|जे द्वारा विकसित प्रिन्सिपिया मैथेमेटिका के प्रस्तावात्मक तर्क के लिए एक कटौती प्रणाली। सी. शॉ. JOHNNIAC पर भी चलने वाली, लॉजिक थ्योरी मशीन ने प्रस्तावात्मक स्वयंसिद्धों के एक छोटे सेट और तीन कटौती नियमों से सबूतों का निर्माण किया: [[मूड सेट करना]], (प्रस्तावात्मक) चर प्रतिस्थापन, और उनकी परिभाषा द्वारा सूत्रों का प्रतिस्थापन। प्रणाली ने अनुमानी मार्गदर्शन का उपयोग किया, और प्रिन्सिपिया के पहले 52 प्रमेयों में से 38 को साबित करने में सफल रही।<ref name=Davis2001/>
[[द्वितीय विश्व युद्ध]] के फौरन बाद, पहले सामान्य प्रयोजन के कंप्यूटर उपलब्ध हो गए। 1954 में, [[मार्टिन डेविस (गणितज्ञ)]] ने प्रिंसटन, न्यू जर्सी में [[उन्नत अध्ययन संस्थान]] में [[JOHNNIAC]] वैक्यूम ट्यूब कंप्यूटर के लिए प्रेस्बर्गर के एल्गोरिदम को प्रोग्राम किया। डेविस के अनुसार इसकी महान विजय यह सिद्ध करना था कि दो सम संख्याओं का योग सम होता है।<ref name=Davis2001/><ref name=Bibel2007>{{cite journal|last=Bibel|first=Wolfgang|title=प्रारंभिक इतिहास और स्वचालित कटौती के परिप्रेक्ष्य|journal=Ki 2007|year=2007|series=LNAI|issue=4667|pages=2–18|url=http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-date=2022-10-09 |url-status=live|access-date=2 September 2012|publisher=Springer}}</ref> 1956 में [[ तर्क सिद्धांत मशीन ]] अधिक महत्वाकांक्षी थी, [[ एलन नेवेल ]], हर्बर्ट ए. साइमन एवं क्लिफ शॉ|जे द्वारा विकसित प्रिन्सिपिया मैथेमेटिका के प्रस्तावात्मक तर्क के लिए एक कटौती प्रणाली। सी. शॉ. JOHNNIAC पर भी चलने वाली, लॉजिक थ्योरी मशीन ने प्रस्तावात्मक स्वयंसिद्धों के एक छोटे सेट एवं तीन कटौती नियमों से सबूतों का निर्माण किया: [[मूड सेट करना]], (प्रस्तावात्मक) चर प्रतिस्थापन, एवं उनकी परिभाषा द्वारा सूत्रों का प्रतिस्थापन। प्रणाली ने अनुमानी मार्गदर्शन का उपयोग किया, एवं प्रिन्सिपिया के पहले 52 प्रमेयों में से 38 को प्रमाणित करने में सफल रही।<ref name=Davis2001/>


लॉजिक थ्योरी मशीन के हेयुरिस्टिक दृष्टिकोण ने मानव गणितज्ञों का अनुकरण करने की कोशिश की, और यह गारंटी नहीं दे सका कि सिद्धांत रूप में भी हर मान्य प्रमेय के लिए एक प्रमाण पाया जा सकता है। इसके विपरीत, अन्य, अधिक व्यवस्थित एल्गोरिदम ने पहले क्रम के तर्क के लिए कम से कम सैद्धांतिक रूप से [[पूर्णता (तर्क)]] हासिल की। आरंभिक दृष्टिकोण हेरब्रांड और स्कोलेम के परिणामों पर भरोसा करते थे ताकि पहले क्रम के फार्मूले को हेरब्रांड ब्रह्मांड से शर्तों के साथ चरों को त्वरित रूप से प्रस्तावित सूत्रों के क्रमिक रूप से बड़े सेटों में परिवर्तित किया जा सके। कई तरीकों का उपयोग करके असंतोषजनकता के लिए प्रस्ताव के सूत्रों की जांच की जा सकती है। गिलमोर के कार्यक्रम ने [[असंबद्ध सामान्य रूप]] में रूपांतरण का उपयोग किया, एक ऐसा रूप जिसमें एक सूत्र की संतुष्टि स्पष्ट है।<ref name=Davis2001/><ref>{{cite journal|last=Gilmore|first=Paul|title=A proof procedure for quantification theory: its justification and realisation|journal=IBM Journal of Research and Development|year=1960|volume=4|pages=28–35|doi=10.1147/rd.41.0028}}</ref>
लॉजिक थ्योरी मशीन के हेयुरिस्टिक दृष्टिकोण ने मानव गणितज्ञों का अनुकरण करने की कोशिश की, एवं यह गारंटी नहीं दे सका कि सिद्धांत रूप में भी हर मान्य प्रमेय के लिए एक प्रमाण पाया जा सकता है। इसके विपरीत, अन्य, अधिक व्यवस्थित एल्गोरिदम ने पहले क्रम के तर्क के लिए कम से कम सैद्धांतिक रूप से [[पूर्णता (तर्क)]] हासिल की। आरंभिक दृष्टिकोण हेरब्रांड एवं स्कोलेम के परिणामों पर भरोसा करते थे ताकि पहले क्रम के फार्मूले को हेरब्रांड ब्रह्मांड से शर्तों के साथ चरों को त्वरित रूप से प्रस्तावित सूत्रों के क्रमिक रूप से बड़े सेटों में परिवर्तित किया जा सके। कई तरीकों का उपयोग करके असंतोषजनकता के लिए प्रस्ताव के सूत्रों की जांच की जा सकती है। गिलमोर के कार्यक्रम ने [[असंबद्ध सामान्य रूप]] में रूपांतरण का उपयोग किया, एक ऐसा रूप जिसमें एक सूत्र की संतुष्टि स्पष्ट है।<ref name=Davis2001/><ref>{{cite journal|last=Gilmore|first=Paul|title=A proof procedure for quantification theory: its justification and realisation|journal=IBM Journal of Research and Development|year=1960|volume=4|pages=28–35|doi=10.1147/rd.41.0028}}</ref>




== समस्या की निश्चितता ==
== समस्या की निश्चितता ==
{{Unreferenced section|date=April 2010}}
{{Unreferenced section|date=April 2010}}
अंतर्निहित तर्क के आधार पर, सूत्र की वैधता तय करने की समस्या तुच्छ से असंभव तक भिन्न होती है। प्रस्तावपरक तर्क के लगातार मामले के लिए, समस्या निर्णायक है लेकिन [[सह-एनपी-पूर्ण]] है, और इसलिए सामान्य सबूत कार्यों के लिए केवल घातीय-समय एल्गोरिदम मौजूद माना जाता है। पहले क्रम के तर्क के लिए, गोडेल की पूर्णता प्रमेय बताती है कि प्रमेय (साबित कथन) तार्किक रूप से मान्य सुनिर्मित सूत्र हैं, इसलिए मान्य सूत्रों की पहचान पुनरावर्ती रूप से गणना योग्य है: असीमित संसाधनों को देखते हुए, कोई भी मान्य सूत्र अंततः सिद्ध किया जा सकता है। हालाँकि, अमान्य फ़ार्मुलों (वे जो किसी दिए गए सिद्धांत में शामिल नहीं हैं) को हमेशा पहचाना नहीं जा सकता है।
अंतर्निहित तर्क के आधार पर, सूत्र की वैधता तय करने की समस्या तुच्छ से असंभव तक भिन्न होती है। प्रस्तावपरक तर्क के लगातार मामले के लिए, समस्या निर्णायक है किन्तु [[सह-एनपी-पूर्ण]] है, एवं इसलिए सामान्य सबूत कार्यों के लिए केवल घातीय-समय एल्गोरिदम मौजूद माना जाता है। पहले क्रम के तर्क के लिए, गोडेल की पूर्णता प्रमेय बताती है कि प्रमेय (प्रमाणित कथन) तार्किक रूप से मान्य सुनिर्मित सूत्र हैं, इसलिए मान्य सूत्रों की पहचान पुनरावर्ती रूप से गणना योग्य है: असीमित संसाधनों को देखते हुए, कोई भी मान्य सूत्र अंततः सिद्ध किया जा सकता है। चूंकि, अमान्य फ़ार्मुलों (वे जो किसी दिए गए सिद्धांत में शामिल नहीं हैं) को हमेशा पहचाना नहीं जा सकता है।


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


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


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


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


[[ सबूत सहायक ]] को सिस्टम को संकेत देने के लिए मानव उपयोगकर्ता की आवश्यकता होती है। स्वचालन की डिग्री के आधार पर, प्रोवर को अनिवार्य रूप से एक प्रूफ चेकर के रूप में कम किया जा सकता है, जिसमें उपयोगकर्ता औपचारिक रूप से [[सबूत संपीड़न]] करता है, या महत्वपूर्ण प्रूफ कार्यों को स्वचालित रूप से निष्पादित किया जा सकता है। इंटरएक्टिव प्रोवर का उपयोग विभिन्न प्रकार के कार्यों के लिए किया जाता है, लेकिन पूरी तरह से स्वचालित प्रणालियों ने भी कई दिलचस्प और कठिन प्रमेयों को साबित किया है, जिसमें कम से कम एक ऐसा है जो लंबे समय तक मानव गणितज्ञों से दूर रहा है, अर्थात् [[रॉबिन्स अनुमान]]।<ref>{{cite journal|first=W.W. |last=McCune|title=रॉबिन्स समस्या का समाधान|journal=Journal of Automated Reasoning|year=1997|volume=19|issue=3|pages=263–276|doi=10.1023/A:1005843212881|s2cid=30847540}}</ref><ref>{{cite news|title=कंप्यूटर मैथ प्रूफ रीज़निंग पावर दिखाता है|author=Gina Kolata|date=December 10, 1996|url=https://www.nytimes.com/library/cyber/week/1210math.html|newspaper=The New York Times|access-date=2008-10-11}}</ref> हालाँकि, ये सफलताएँ छिटपुट हैं, और कठिन समस्याओं पर काम करने के लिए आमतौर पर एक कुशल उपयोगकर्ता की आवश्यकता होती है।
[[ सबूत सहायक ]] को सिस्टम को संकेत देने के लिए मानव उपयोगकर्ता की आवश्यकता होती है। स्वचालन की डिग्री के आधार पर, प्रोवर को अनिवार्य रूप से एक प्रूफ चेकर के रूप में कम किया जा सकता है, जिसमें उपयोगकर्ता औपचारिक रूप से [[सबूत संपीड़न]] करता है, या महत्वपूर्ण प्रूफ कार्यों को स्वचालित रूप से निष्पादित किया जा सकता है। इंटरएक्टिव प्रोवर का उपयोग विभिन्न प्रकार के कार्यों के लिए किया जाता है, किन्तु पूरी तरह से स्वचालित प्रणालियों ने भी कई दिलचस्प एवं कठिन प्रमेयों को प्रमाणित किया है, जिसमें कम से कम एक ऐसा है जो लंबे समय तक मानव गणितज्ञों से दूर रहा है, अर्थात् [[रॉबिन्स अनुमान]]।<ref>{{cite journal|first=W.W. |last=McCune|title=रॉबिन्स समस्या का समाधान|journal=Journal of Automated Reasoning|year=1997|volume=19|issue=3|pages=263–276|doi=10.1023/A:1005843212881|s2cid=30847540}}</ref><ref>{{cite news|title=कंप्यूटर मैथ प्रूफ रीज़निंग पावर दिखाता है|author=Gina Kolata|date=December 10, 1996|url=https://www.nytimes.com/library/cyber/week/1210math.html|newspaper=The New York Times|access-date=2008-10-11}}</ref> चूंकि, ये सफलताएँ छिटपुट हैं, एवं कठिन समस्याओं पर काम करने के लिए आमतौर पर एक कुशल उपयोगकर्ता की आवश्यकता होती है।


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


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


== औद्योगिक उपयोग ==
== औद्योगिक उपयोग ==
{{Unreferenced section|date=July 2020}}
{{Unreferenced section|date=July 2020}}
स्वचालित प्रमेय साबित करने का व्यावसायिक उपयोग ज्यादातर [[एकीकृत सर्किट डिजाइन]] और सत्यापन में केंद्रित है। [[पेंटियम FDIV बग]] के बाद से, आधुनिक माइक्रोप्रोसेसरों की जटिल [[फ्लोटिंग पॉइंट यूनिट]] को अतिरिक्त जांच के साथ डिज़ाइन किया गया है। [[एएमडी]], [[इंटेल]] और अन्य स्वचालित प्रमेय का उपयोग यह सत्यापित करने के लिए करते हैं कि विभाजन और अन्य संचालन उनके प्रोसेसर में सही ढंग से लागू किए गए हैं।
स्वचालित प्रमेय प्रमाणित करने का व्यावसायिक उपयोग ज्यादातर [[एकीकृत सर्किट डिजाइन]] एवं सत्यापन में केंद्रित है। [[पेंटियम FDIV बग]] के बाद से, आधुनिक माइक्रोप्रोसेसरों की जटिल [[फ्लोटिंग पॉइंट यूनिट]] को अतिरिक्त जांच के साथ डिज़ाइन किया गया है। [[एएमडी]], [[इंटेल]] एवं अन्य स्वचालित प्रमेय का उपयोग यह सत्यापित करने के लिए करते हैं कि विभाजन एवं अन्य संचालन उनके प्रोसेसर में सही ढंग से लागू किए गए हैं।


== प्रथम-क्रम प्रमेय साबित कर रहा है ==
== प्रथम-क्रम प्रमेय प्रमाणित कर रहा है ==
{{more citations needed section|date=July 2020}}
{{more citations needed section|date=July 2020}}
1960 के दशक के अंत में स्वचालित कटौती में अनुसंधान को वित्तपोषित करने वाली एजेंसियों ने व्यावहारिक अनुप्रयोगों की आवश्यकता पर जोर देना शुरू किया। पहले फलदायी क्षेत्रों में से एक [[कार्यक्रम सत्यापन]] का था जिसके द्वारा पास्कल, एडा, आदि जैसी भाषाओं में कंप्यूटर प्रोग्राम की शुद्धता की पुष्टि करने की समस्या के लिए प्रथम-क्रम प्रमेय प्रवर्तकों को लागू किया गया था। प्रारंभिक कार्यक्रम सत्यापन प्रणालियों में उल्लेखनीय स्टैनफोर्ड पास्कल सत्यापनकर्ता था। [[स्टैनफोर्ड विश्वविद्यालय]] में [[डेविड लकहम]] द्वारा विकसित।<ref>{{cite report | url=https://apps.dtic.mil/sti/citations/ADA027455 | archive-url=https://web.archive.org/web/20210812180903/https://apps.dtic.mil/sti/citations/ADA027455 | url-status=live | archive-date=August 12, 2021 | author=David C. Luckham and Norihisa Suzuki | title=Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers | institution=[[Defense Technical Information Center]] | type=Technical Report AD-A027 455 | date=Mar 1976 }}</ref><ref>{{cite journal | doi=10.1145/357073.357078 | first1=David C. |last1=Luckham |first2=Norihisa |last2=Suzuki | title=पास्कल में ऐरे, रिकॉर्ड और पॉइंटर ऑपरेशंस का सत्यापन| journal=[[ACM Transactions on Programming Languages and Systems]] | volume=1 | number=2 | pages=226–244 | date=Oct 1979 | s2cid=10088183 | doi-access=free }}</ref><ref>{{cite techreport | url=https://exhibits.stanford.edu/stanford-pubs/catalog/nh154bt5645 |first1=D. |last1=Luckham |first2=S. |last2=German |first3=F. |last3=von Henke |first4=R. |last4=Karp |first5=P. |last5=Milne |first6=D. |last6=Oppen |first7=W. |last7=Polak |first8=W. |last8=Scherlis | title=स्टैनफोर्ड पास्कल सत्यापनकर्ता उपयोगकर्ता पुस्तिका| institution=Stanford University | id=CS-TR-79-731 | year=1979 }}</ref> यह [[जॉन एलन रॉबिन्सन]] के [[संकल्प (तर्क)]] सिद्धांत का उपयोग करके स्टैनफोर्ड में विकसित स्टैनफोर्ड रिज़ॉल्यूशन प्रोवर पर भी आधारित था। यह गणितीय समस्याओं को हल करने की क्षमता प्रदर्शित करने वाली पहली स्वचालित कटौती प्रणाली थी, जो समाधान औपचारिक रूप से प्रकाशित होने से पहले अमेरिकन मैथमैटिकल सोसाइटी के नोटिस में घोषित की गई थी।{{citation needed|date=September 2020}}
1960 के दशक के अंत में स्वचालित कटौती में अनुसंधान को वित्तपोषित करने वाली एजेंसियों ने व्यावहारिक अनुप्रयोगों की आवश्यकता पर जोर देना शुरू किया। पहले फलदायी क्षेत्रों में से एक [[कार्यक्रम सत्यापन]] का था जिसके द्वारा पास्कल, एडा, आदि जैसी भाषाओं में कंप्यूटर प्रोग्राम की शुद्धता की पुष्टि करने की समस्या के लिए प्रथम-क्रम प्रमेय प्रवर्तकों को लागू किया गया था। प्रारंभिक कार्यक्रम सत्यापन प्रणालियों में उल्लेखनीय स्टैनफोर्ड पास्कल सत्यापनकर्ता था। [[स्टैनफोर्ड विश्वविद्यालय]] में [[डेविड लकहम]] द्वारा विकसित।<ref>{{cite report | url=https://apps.dtic.mil/sti/citations/ADA027455 | archive-url=https://web.archive.org/web/20210812180903/https://apps.dtic.mil/sti/citations/ADA027455 | url-status=live | archive-date=August 12, 2021 | author=David C. Luckham and Norihisa Suzuki | title=Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers | institution=[[Defense Technical Information Center]] | type=Technical Report AD-A027 455 | date=Mar 1976 }}</ref><ref>{{cite journal | doi=10.1145/357073.357078 | first1=David C. |last1=Luckham |first2=Norihisa |last2=Suzuki | title=पास्कल में ऐरे, रिकॉर्ड और पॉइंटर ऑपरेशंस का सत्यापन| journal=[[ACM Transactions on Programming Languages and Systems]] | volume=1 | number=2 | pages=226–244 | date=Oct 1979 | s2cid=10088183 | doi-access=free }}</ref><ref>{{cite techreport | url=https://exhibits.stanford.edu/stanford-pubs/catalog/nh154bt5645 |first1=D. |last1=Luckham |first2=S. |last2=German |first3=F. |last3=von Henke |first4=R. |last4=Karp |first5=P. |last5=Milne |first6=D. |last6=Oppen |first7=W. |last7=Polak |first8=W. |last8=Scherlis | title=स्टैनफोर्ड पास्कल सत्यापनकर्ता उपयोगकर्ता पुस्तिका| institution=Stanford University | id=CS-TR-79-731 | year=1979 }}</ref> यह [[जॉन एलन रॉबिन्सन]] के [[संकल्प (तर्क)]] सिद्धांत का उपयोग करके स्टैनफोर्ड में विकसित स्टैनफोर्ड रिज़ॉल्यूशन प्रोवर पर भी आधारित था। यह गणितीय समस्याओं को हल करने की क्षमता प्रदर्शित करने वाली प्रथम स्वचालित कटौती प्रणाली थी, जो समाधान औपचारिक रूप से प्रकाशित होने से पहले अमेरिकन मैथमैटिकल सोसाइटी के नोटिस में घोषित की गई थी।{{citation needed|date=September 2020}}


प्रथम-क्रम तर्क | प्रथम-क्रम प्रमेय साबित करना स्वचालित प्रमेय साबित करने के सबसे परिपक्व उपक्षेत्रों में से एक है। तर्क पर्याप्त अभिव्यंजक है जो मनमाना समस्याओं के विनिर्देशन की अनुमति देता है, अक्सर एक यथोचित प्राकृतिक और सहज तरीके से। दूसरी ओर, यह अभी भी अर्ध-निर्णायक है, और पूरी तरह से स्वचालित प्रणालियों को सक्षम करने के लिए कई ध्वनि और पूर्ण कैलकुली विकसित की गई हैं।<ref>{{Cite journal|last=Loveland|first=D W|date=1986|title=Automated theorem proving: mapping logic into AI|url=http://portal.acm.org/citation.cfm?doid=12808.12833|journal=Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems |language=en|location=Knoxville, Tennessee, United States|publisher=ACM Press|page=224|doi=10.1145/12808.12833|isbn=978-0-89791-206-8|s2cid=14361631|doi-access=free}}</ref> अधिक अभिव्यंजक तर्क, जैसे [[उच्च-क्रम तर्क]], प्रथम क्रम तर्क की तुलना में समस्याओं की एक विस्तृत श्रृंखला की सुविधाजनक अभिव्यक्ति की अनुमति देते हैं, लेकिन इन तर्कों के लिए सिद्ध करने वाला प्रमेय कम विकसित है।<ref>Kerber, Manfred. "[https://kluedo.ub.uni-kl.de/files/364/seki_4.pdf How to prove higher order theorems in first order logic]." (1999).</ref><ref>Benzmüller, Christoph, et al. "[https://page.mi.fu-berlin.de/cbenzmueller/papers/C26.pdf LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)]." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2008.</ref>
प्रथम-क्रम तर्क | प्रथम-क्रम प्रमेय प्रमाणित करना स्वचालित प्रमेय प्रमाणित करने के सबसे परिपक्व उपक्षेत्रों में से एक है। तर्क पर्याप्त अभिव्यंजक है जो मनमाना समस्याओं के विनिर्देशन की अनुमति देता है, अक्सर एक यथोचित प्राकृतिक एवं सहज तरीके से। दूसरी ओर, यह अभी भी अर्ध-निर्णायक है, एवं पूरी तरह से स्वचालित प्रणालियों को सक्षम करने के लिए कई ध्वनि एवं पूर्ण कैलकुली विकसित की गई हैं।<ref>{{Cite journal|last=Loveland|first=D W|date=1986|title=Automated theorem proving: mapping logic into AI|url=http://portal.acm.org/citation.cfm?doid=12808.12833|journal=Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems |language=en|location=Knoxville, Tennessee, United States|publisher=ACM Press|page=224|doi=10.1145/12808.12833|isbn=978-0-89791-206-8|s2cid=14361631|doi-access=free}}</ref> अधिक अभिव्यंजक तर्क, जैसे [[उच्च-क्रम तर्क]], प्रथम क्रम तर्क की तुलना में समस्याओं की एक विस्तृत श्रृंखला की सुविधाजनक अभिव्यक्ति की अनुमति देते हैं, किन्तु इन तर्कों के लिए सिद्ध करने वाला प्रमेय कम विकसित है।<ref>Kerber, Manfred. "[https://kluedo.ub.uni-kl.de/files/364/seki_4.pdf How to prove higher order theorems in first order logic]." (1999).</ref><ref>Benzmüller, Christoph, et al. "[https://page.mi.fu-berlin.de/cbenzmueller/papers/C26.pdf LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)]." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2008.</ref>




== बेंचमार्क, प्रतियोगिताएं, और स्रोत ==
== बेंचमार्क, प्रतियोगिताएं, एवं स्रोत ==
मानक बेंचमार्क उदाहरणों के एक बड़े पुस्तकालय के अस्तित्व से कार्यान्वित प्रणालियों की गुणवत्ता को लाभ हुआ है - थ्योरम प्रोवर्स (टीपीटीपी) प्रॉब्लम लाइब्रेरी के लिए हजारों समस्याएं<ref>{{cite web|last=Sutcliffe|first=Geoff|title=स्वचालित प्रमेय साबित करने के लिए टीपीटीपी समस्या पुस्तकालय|url=http://www.tptp.org/|access-date=15 July 2019}}</ref> - साथ ही सीएडीई [[कैड एटीपी सिस्टम प्रतियोगिता]]सीएएससी) से, फर्स्ट-ऑर्डर समस्याओं के कई महत्वपूर्ण वर्गों के लिए फर्स्ट-ऑर्डर सिस्टम की वार्षिक प्रतियोगिता।
मानक बेंचमार्क उदाहरणों के एक बड़े पुस्तकालय के अस्तित्व से कार्यान्वित प्रणालियों की गुणवत्ता को लाभ हुआ है - थ्योरम प्रोवर्स (टीपीटीपी) प्रॉब्लम लाइब्रेरी के लिए हजारों समस्याएं<ref>{{cite web|last=Sutcliffe|first=Geoff|title=स्वचालित प्रमेय साबित करने के लिए टीपीटीपी समस्या पुस्तकालय|url=http://www.tptp.org/|access-date=15 July 2019}}</ref> - साथ ही सीएडीई [[कैड एटीपी सिस्टम प्रतियोगिता]]सीएएससी) से, फर्स्ट-ऑर्डर समस्याओं के कई महत्वपूर्ण वर्गों के लिए फर्स्ट-ऑर्डर सिस्टम की वार्षिक प्रतियोगिता।


कुछ महत्वपूर्ण प्रणालियाँ (सभी ने कम से कम एक CASC प्रतियोगिता प्रभाग जीता है) नीचे सूचीबद्ध हैं।
कुछ महत्वपूर्ण प्रणालियाँ (सभी ने कम से कम एक CASC प्रतियोगिता प्रभाग जीता है) नीचे सूचीबद्ध हैं।
* ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, लेकिन एक [[सुपरपोजिशन कैलकुलस]] पर बनाया गया है, मूल रूप से [[वोल्फगैंग बाइबिल]] के निर्देशन में [[म्यूनिख के तकनीकी विश्वविद्यालय]] के स्वचालित तर्क समूह में विकसित किया गया था, और अब बाडेन-वुर्टेमबर्ग सहकारी में [[ स्टटगर्ट ]] में स्टेट यूनिवर्सिटी।
* ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, किन्तु एक [[सुपरपोजिशन कैलकुलस]] पर बनाया गया है, मूल रूप से [[वोल्फगैंग बाइबिल]] के निर्देशन में [[म्यूनिख के तकनीकी विश्वविद्यालय]] के स्वचालित तर्क समूह में विकसित किया गया था, एवं अब बाडेन-वुर्टेमबर्ग सहकारी में [[ स्टटगर्ट ]] में स्टेट यूनिवर्सिटी।
* ऊदबिलाव (प्रमेय प्रमेय), [[Argonne राष्ट्रीय प्रयोगशाला]] में विकसित, प्रथम क्रम संकल्प और [[paramodulation]] पर आधारित है। तब से ओटर को [[Prover9]] द्वारा प्रतिस्थापित कर दिया गया है, जिसे [[Mace4]] के साथ जोड़ा गया है।
* ऊदबिलाव (प्रमेय प्रमेय), [[Argonne राष्ट्रीय प्रयोगशाला]] में विकसित, प्रथम क्रम संकल्प एवं [[paramodulation]] पर आधारित है। तब से ओटर को [[Prover9]] द्वारा प्रतिस्थापित कर दिया गया है, जिसे [[Mace4]] के साथ जोड़ा गया है।
* [[SETHEO]] लक्ष्य-निर्देशित [[ मॉडल उन्मूलन ]] कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E और SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो साबित करता है<nowiki/>r E-SETHEO।
* [[SETHEO]] लक्ष्य-निर्देशित [[ मॉडल उन्मूलन ]] कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो प्रमाणित करत<nowiki/>ा हैr E-SETHEO।
* वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव और क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित और कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है।
* वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित एवं कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है।
* वाल्डमिस्टर अर्निम बुच और थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने लगातार चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता।
* वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने लगातार चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता।
* [[SPASS]] समानता के साथ एक प्रथम क्रम तर्क प्रमेय है। इसे रिसर्च ग्रुप ऑटोमेशन ऑफ लॉजिक, [[कंप्यूटर विज्ञान के लिए मैक्स प्लैंक संस्थान]] द्वारा विकसित किया गया है।
* [[SPASS]] समानता के साथ एक प्रथम क्रम तर्क प्रमेय है। इसे रिसर्च ग्रुप ऑटोमेशन ऑफ लॉजिक, [[कंप्यूटर विज्ञान के लिए मैक्स प्लैंक संस्थान]] द्वारा विकसित किया गया है।


Line 69: Line 67:
* मॉडल उन्मूलन
* मॉडल उन्मूलन
*[[विश्लेषणात्मक झांकी की विधि]]
*[[विश्लेषणात्मक झांकी की विधि]]
*सुपरपोजिशन कैलकुलस और टर्म [[पुनर्लेखन]]
*सुपरपोजिशन कैलकुलस एवं टर्म [[पुनर्लेखन]]
* मॉडल जाँच
* मॉडल जाँच
*[[गणितीय प्रेरण]]<ref>{{cite techreport |first=Alan |last=Bundy |title=गणितीय प्रेरण द्वारा प्रमाण का स्वचालन|date=1999 |publisher=Division of Informatics, University of Edinburgh|url=https://www.era.lib.ed.ac.uk/bitstream/handle/1842/3394/0002.pdf?sequence=1 |hdl=1842/3394  |series=Informatics Research Report |volume=2}}</ref>
*[[गणितीय प्रेरण]]<ref>{{cite techreport |first=Alan |last=Bundy |title=गणितीय प्रेरण द्वारा प्रमाण का स्वचालन|date=1999 |publisher=Division of Informatics, University of Edinburgh|url=https://www.era.lib.ed.ac.uk/bitstream/handle/1842/3394/0002.pdf?sequence=1 |hdl=1842/3394  |series=Informatics Research Report |volume=2}}</ref>

Revision as of 15:30, 19 May 2023

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

तार्किक नींव

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

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

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

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


समस्या की निश्चितता

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

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

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

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

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

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

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

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

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

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

प्रथम-क्रम प्रमेय प्रमाणित कर रहा है

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

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


बेंचमार्क, प्रतियोगिताएं, एवं स्रोत

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

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

  • ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, किन्तु एक सुपरपोजिशन कैलकुलस पर बनाया गया है, मूल रूप से वोल्फगैंग बाइबिल के निर्देशन में म्यूनिख के तकनीकी विश्वविद्यालय के स्वचालित तर्क समूह में विकसित किया गया था, एवं अब बाडेन-वुर्टेमबर्ग सहकारी में स्टटगर्ट में स्टेट यूनिवर्सिटी।
  • ऊदबिलाव (प्रमेय प्रमेय), Argonne राष्ट्रीय प्रयोगशाला में विकसित, प्रथम क्रम संकल्प एवं paramodulation पर आधारित है। तब से ओटर को Prover9 द्वारा प्रतिस्थापित कर दिया गया है, जिसे Mace4 के साथ जोड़ा गया है।
  • SETHEO लक्ष्य-निर्देशित मॉडल उन्मूलन कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो प्रमाणित करता हैr E-SETHEO।
  • वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा मैनचेस्टर विश्वविद्यालय में विकसित एवं कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है।
  • वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने लगातार चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता।
  • 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
KeYmaera GPL Via Java Webstart Yes Yes March 11, 2015
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 (in English). 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.


संदर्भ


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=स्वचालित_प्रमेय_प्रमाणन&oldid=170223’