स्वचालित प्रमेय प्रमाणन: Difference between revisions
No edit summary |
No edit summary |
||
| Line 21: | Line 21: | ||
== समस्या की निश्चितता == | == समस्या की निश्चितता == | ||
अंतर्निहित तर्क के आधार पर, सूत्र की वैधता निर्धारित करने की समस्या तुच्छ से असंभव तक भिन्न होती है। प्रस्तावपरक तर्क के निरंतर विषय के लिए, समस्या निर्णायक है किन्तु [[सह-एनपी-पूर्ण]] है, एवं इसलिए सामान्य प्रमाण कार्यों के लिए केवल घातीय-समय एल्गोरिदम उपस्थित माना जाता है। | अंतर्निहित तर्क के आधार पर, सूत्र की वैधता निर्धारित करने की समस्या तुच्छ से असंभव तक भिन्न होती है। प्रस्तावपरक तर्क के निरंतर विषय के लिए, समस्या निर्णायक है किन्तु [[सह-एनपी-पूर्ण]] है, एवं इसलिए सामान्य प्रमाण कार्यों के लिए केवल घातीय-समय एल्गोरिदम उपस्थित माना जाता है। प्रथम क्रम के तर्क के लिए, गोडेल की पूर्णता प्रमेय बताती है कि प्रमेय (प्रमाणित कथन) तार्किक रूप से मान्य सुनिर्मित सूत्र हैं, इसलिए मान्य सूत्रों की पहचान पुनरावर्ती रूप से गणना योग्य है: असीमित संसाधनों को देखते हुए, कोई भी मान्य सूत्र अंततः सिद्ध किया जा सकता है। चूंकि, अमान्य फ़ार्मुलों (वे जो किसी दिए गए सिद्धांत में सम्मिलित नहीं हैं) को सदैव पहचाना नहीं जा सकता है। | ||
उपरोक्त | उपरोक्त प्रथम क्रम के सिद्धांतों पर प्रारम्भ होता है, जैसे कि पियानो स्वयं सिद्ध चूंकि, विशिष्ट प्रतिरूप के लिए जिसे पूर्व आदेश सिद्धांत द्वारा वर्णित किया जा सकता है, कुछ कथन सत्य हो सकते हैं किन्तु प्रतिरूप का वर्णन करने के लिए उपयोग किए जाने वाले सिद्धांत में अनिर्णीत हो सकते हैं। उदाहरण के लिए, गोडेल के अपूर्णता प्रमेय के द्वारा, हम जानते हैं कि कोई भी सिद्धांत जिसका उचित अभिगृहीत प्राकृतिक संख्याओं के लिए सत्य है, प्राकृतिक संख्याओं के लिए प्रथम क्रम के सभी कथनों को सत्य प्रमाणित नहीं कर सकता है, भले ही उचित अभिगृहीतों की सूची अनंत गणनीय हो। यह इस प्रकार है कि स्वचालित प्रमेय समर्थक प्रमाण का शोध करते समय ठीक से समाप्त करने में असफल हो जाएगा, जब परिक्षण किये जा रहे वर्णन सिद्धांत में अनिर्णीत है, भले ही यह ब्याज के प्रतिरूप में सच हो। इस सैद्धांतिक सीमा के पश्चात भी व्यवहार में, प्रमेय समर्थक कई कठिन समस्याओं का समाधान कर सकते हैं, यहां तक कि उन प्रतिरूपों में भी जो किसी भी प्रथम आदेश सिद्धांत (जैसे पूर्णांक) द्वारा पूर्ण रूप से वर्णित नहीं हैं। | ||
== संबंधित समस्याएं == | == संबंधित समस्याएं == | ||
एक सरल, किन्तु संबंधित, समस्या [[प्रमाण सत्यापन]] है, जहां एक प्रमेय के लिए मौजूदा प्रमाण मान्य प्रमाणित है। इसके लिए, आम तौर पर यह आवश्यक है कि प्रत्येक अलग-अलग प्रमाण चरण को एक आदिम पुनरावर्ती फ़ंक्शन या प्रोग्राम द्वारा सत्यापित किया जा सके, एवं इसलिए समस्या | एक सरल, किन्तु संबंधित, समस्या [[प्रमाण सत्यापन]] है, जहां एक प्रमेय के लिए मौजूदा प्रमाण मान्य प्रमाणित है। इसके लिए, आम तौर पर यह आवश्यक है कि प्रत्येक अलग-अलग प्रमाण चरण को एक आदिम पुनरावर्ती फ़ंक्शन या प्रोग्राम द्वारा सत्यापित किया जा सके, एवं इसलिए समस्या सदैव निर्णायक होती है। | ||
चूंकि स्वचालित प्रमेय सिद्धकर्ताओं द्वारा उत्पन्न प्रमाण आम तौर पर बहुत बड़े होते हैं, प्रमाण संपीड़न की समस्या महत्वपूर्ण है एवं विभिन्न तकनीकों का लक्ष्य है कि प्रस्तावक के आउटपुट को छोटा बनाया जाए, एवं परिणामस्वरूप अधिक आसानी से समझा जा सके एवं | चूंकि स्वचालित प्रमेय सिद्धकर्ताओं द्वारा उत्पन्न प्रमाण आम तौर पर बहुत बड़े होते हैं, प्रमाण संपीड़न की समस्या महत्वपूर्ण है एवं विभिन्न तकनीकों का लक्ष्य है कि प्रस्तावक के आउटपुट को छोटा बनाया जाए, एवं परिणामस्वरूप अधिक आसानी से समझा जा सके एवं परिक्षणा जा सके। | ||
[[ सबूत सहायक | प्रमाण सहायक]] को सिस्टम को संकेत देने के लिए मानव उपयोगकर्ता की आवश्यकता होती है। स्वचालन की डिग्री के आधार पर, प्रोवर को अनिवार्य रूप से एक प्रूफ चेकर के रूप में कम किया जा सकता है, जिसमें उपयोगकर्ता औपचारिक रूप से [[सबूत संपीड़न|प्रमाण संपीड़न]] करता है, या महत्वपूर्ण प्रूफ कार्यों को स्वचालित रूप से निष्पादित किया जा सकता है। इंटरएक्टिव प्रोवर का उपयोग विभिन्न प्रकार के कार्यों के लिए किया जाता है, किन्तु पूरी तरह से स्वचालित प्रणालियों ने भी कई दिलचस्प एवं कठिन प्रमेयों को प्रमाणित किया है, जिसमें कम से कम एक ऐसा है जो लंबे समय तक मानव गणितज्ञों से दूर रहा है, अर्थात् [[रॉबिन्स अनुमान]]।<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> चूंकि, ये सफलताएँ छिटपुट हैं, एवं कठिन समस्याओं पर काम करने के लिए आमतौर पर एक कुशल उपयोगकर्ता की आवश्यकता होती है। | ||
कभी-कभी प्रमेय सिद्ध करने एवं अन्य तकनीकों के बीच एक एवं अंतर निकाला जाता है, जहां एक प्रक्रिया को प्रमेय प्रमाणित करने के लिए माना जाता है, अगर इसमें एक पारंपरिक प्रमाण होता है, जो स्वयंसिद्धों से शुरू होता है एवं अनुमान के नियमों का उपयोग करके नए अनुमान के चरणों का निर्माण करता है। अन्य तकनीकों में [[मॉडल की जाँच]] | कभी-कभी प्रमेय सिद्ध करने एवं अन्य तकनीकों के बीच एक एवं अंतर निकाला जाता है, जहां एक प्रक्रिया को प्रमेय प्रमाणित करने के लिए माना जाता है, अगर इसमें एक पारंपरिक प्रमाण होता है, जो स्वयंसिद्धों से शुरू होता है एवं अनुमान के नियमों का उपयोग करके नए अनुमान के चरणों का निर्माण करता है। अन्य तकनीकों में [[मॉडल की जाँच|प्रतिरूप की परिक्षण]] सम्मिलित होगी, जिसमें, सबसे सरल मामले में, कई संभावित राज्यों की क्रूर-बल गणना सम्मिलित है (चूंकि प्रतिरूप चेकर्स के वास्तविक कार्यान्वयन के लिए बहुत चतुराई की आवश्यकता होती है, एवं यह केवल क्रूर बल को कम नहीं करता है)। | ||
हाइब्रिड प्रमेय प्रमाणित करने वाली प्रणालियाँ हैं जो एक अनुमान नियम के रूप में | हाइब्रिड प्रमेय प्रमाणित करने वाली प्रणालियाँ हैं जो एक अनुमान नियम के रूप में प्रतिरूप परिक्षण का उपयोग करती हैं। ऐसे प्रोग्राम भी हैं जो एक विशेष प्रमेय को सिद्ध करने के लिए लिखे गए थे, एक (आमतौर पर अनौपचारिक) प्रमाण के साथ कि यदि कार्यक्रम एक निश्चित परिणाम के साथ समाप्त होता है, तो प्रमेय सत्य है। इसका एक अच्छा उदाहरण [[चार रंग प्रमेय]] का मशीन-समर्थित प्रमाण था, जो पहले दावा किए गए गणितीय प्रमाण के रूप में बहुत विवादास्पद था जिसे कार्यक्रम की गणना के विशाल आकार के कारण मनुष्यों द्वारा सत्यापित करना अनिवार्य रूप से असंभव था (ऐसे प्रमाणों को गैर कहा जाता है) -सर्वे योग्य प्रमाण)। प्रोग्राम-समर्थित प्रमाण का एक एवं उदाहरण वह है जो दिखाता है कि [[ चार कनेक्ट करें ]] का खेल सदैव पहले खिलाड़ी द्वारा जीता जा सकता है। | ||
== औद्योगिक उपयोग == | == औद्योगिक उपयोग == | ||
स्वचालित प्रमेय प्रमाणित करने का व्यावसायिक उपयोग ज्यादातर [[एकीकृत सर्किट डिजाइन]] एवं सत्यापन में केंद्रित है। [[पेंटियम FDIV बग]] के बाद से, आधुनिक माइक्रोप्रोसेसरों की जटिल [[फ्लोटिंग पॉइंट यूनिट]] को अतिरिक्त | स्वचालित प्रमेय प्रमाणित करने का व्यावसायिक उपयोग ज्यादातर [[एकीकृत सर्किट डिजाइन]] एवं सत्यापन में केंद्रित है। [[पेंटियम FDIV बग]] के बाद से, आधुनिक माइक्रोप्रोसेसरों की जटिल [[फ्लोटिंग पॉइंट यूनिट]] को अतिरिक्त परिक्षण के साथ डिज़ाइन किया गया है। [[एएमडी]], [[इंटेल]] एवं अन्य स्वचालित प्रमेय का उपयोग यह सत्यापित करने के लिए करते हैं कि विभाजन एवं अन्य संचालन उनके प्रोसेसर में सही ढंग से प्रारम्भ किए गए हैं। | ||
== प्रथम-क्रम प्रमेय प्रमाणित कर रहा है == | == प्रथम-क्रम प्रमेय प्रमाणित कर रहा है == | ||
1960 के दशक के अंत में स्वचालित कटौती में अनुसंधान को वित्तपोषित करने वाली एजेंसियों ने व्यावहारिक अनुप्रयोगों की आवश्यकता पर जोर देना शुरू किया। पहले फलदायी क्षेत्रों में से एक [[कार्यक्रम सत्यापन]] का था जिसके द्वारा पास्कल, एडा, आदि जैसी भाषाओं में कंप्यूटर प्रोग्राम की शुद्धता की पुष्टि करने की समस्या के लिए प्रथम-क्रम प्रमेय प्रवर्तकों को | 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> | ||
| Line 52: | Line 52: | ||
* ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, किन्तु एक [[सुपरपोजिशन कैलकुलस]] पर बनाया गया है, मूल रूप से [[वोल्फगैंग बाइबिल]] के निर्देशन में [[म्यूनिख के तकनीकी विश्वविद्यालय]] के स्वचालित तर्क समूह में विकसित किया गया था, एवं अब बाडेन-वुर्टेमबर्ग सहकारी में [[ स्टटगर्ट ]] में स्टेट यूनिवर्सिटी। | * ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, किन्तु एक [[सुपरपोजिशन कैलकुलस]] पर बनाया गया है, मूल रूप से [[वोल्फगैंग बाइबिल]] के निर्देशन में [[म्यूनिख के तकनीकी विश्वविद्यालय]] के स्वचालित तर्क समूह में विकसित किया गया था, एवं अब बाडेन-वुर्टेमबर्ग सहकारी में [[ स्टटगर्ट ]] में स्टेट यूनिवर्सिटी। | ||
* ऊदबिलाव (प्रमेय प्रमेय), [[Argonne राष्ट्रीय प्रयोगशाला]] में विकसित, प्रथम क्रम संकल्प एवं [[paramodulation]] पर आधारित है। तब से ओटर को [[Prover9]] द्वारा प्रतिस्थापित कर दिया गया है, जिसे [[Mace4]] के साथ जोड़ा गया है। | * ऊदबिलाव (प्रमेय प्रमेय), [[Argonne राष्ट्रीय प्रयोगशाला]] में विकसित, प्रथम क्रम संकल्प एवं [[paramodulation]] पर आधारित है। तब से ओटर को [[Prover9]] द्वारा प्रतिस्थापित कर दिया गया है, जिसे [[Mace4]] के साथ जोड़ा गया है। | ||
* [[SETHEO]] लक्ष्य-निर्देशित [[ मॉडल उन्मूलन ]] कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो प्रमाणित | * [[SETHEO]] लक्ष्य-निर्देशित [[ मॉडल उन्मूलन | प्रतिरूप उन्मूलन]] कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो प्रमाणित<nowiki/> करता हैr E-SETHEO। | ||
* वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित एवं कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है। | * वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित एवं कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है। | ||
* वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने निरंतर चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता। | * वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने निरंतर चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता। | ||
| Line 62: | Line 62: | ||
*एकीकरण के साथ प्रथम क्रम संकल्प (कंप्यूटिंग) | *एकीकरण के साथ प्रथम क्रम संकल्प (कंप्यूटिंग) | ||
* | * प्रतिरूप उन्मूलन | ||
*[[विश्लेषणात्मक झांकी की विधि]] | *[[विश्लेषणात्मक झांकी की विधि]] | ||
*सुपरपोजिशन कैलकुलस एवं टर्म [[पुनर्लेखन]] | *सुपरपोजिशन कैलकुलस एवं टर्म [[पुनर्लेखन]] | ||
* | * प्रतिरूप परिक्षण | ||
*[[गणितीय प्रेरण]]<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:58, 19 May 2023
स्वचालित प्रमेय प्रमाणित करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) स्वचालित तर्क एवं गणितीय तर्क का उपक्षेत्र है जो कंप्यूटर प्रोग्राम द्वारा गणितीय प्रमेय को प्रमाणित करने से संबंधित है। गणितीय प्रमाण पर स्वचालित तर्क कंप्यूटर विज्ञान के विकास के लिए प्रमुख प्रेरणा थी।
तार्किक नींव
जबकि औपचारिक तर्कवाद की जड़ें अरिस्टोटेलियन तर्क में वापस जाती हैं, 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 प्रतियोगिता प्रभाग जीता है) नीचे सूचीबद्ध हैं।
- ई प्रमेय प्रस्तावक पूर्ण प्रथम-क्रम तर्क के लिए एक उच्च-प्रदर्शन वाला प्रस्तावक है, किन्तु एक सुपरपोजिशन कैलकुलस पर बनाया गया है, मूल रूप से वोल्फगैंग बाइबिल के निर्देशन में म्यूनिख के तकनीकी विश्वविद्यालय के स्वचालित तर्क समूह में विकसित किया गया था, एवं अब बाडेन-वुर्टेमबर्ग सहकारी में स्टटगर्ट में स्टेट यूनिवर्सिटी।
- ऊदबिलाव (प्रमेय प्रमेय), Argonne राष्ट्रीय प्रयोगशाला में विकसित, प्रथम क्रम संकल्प एवं paramodulation पर आधारित है। तब से ओटर को Prover9 द्वारा प्रतिस्थापित कर दिया गया है, जिसे Mace4 के साथ जोड़ा गया है।
- SETHEO लक्ष्य-निर्देशित प्रतिरूप उन्मूलन कैलकुलस पर आधारित एक उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में एक टीम द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो प्रमाणित करता हैr E-SETHEO।
- वैम्पायर प्रमेय कहावत मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा मैनचेस्टर विश्वविद्यालय में विकसित एवं कार्यान्वित की गई थी। यह अब एक बढ़ती अंतरराष्ट्रीय टीम द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी सिस्टम प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के बीच) जीता है।
- वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए एक विशेष प्रणाली है। इसने निरंतर चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन जीता।
- SPASS समानता के साथ एक प्रथम क्रम तर्क प्रमेय है। इसे रिसर्च ग्रुप ऑटोमेशन ऑफ लॉजिक, कंप्यूटर विज्ञान के लिए मैक्स प्लैंक संस्थान द्वारा विकसित किया गया है।
प्रमेय प्रोवर संग्रहालय[19] भविष्य के विश्लेषण के लिए थ्योरम प्रोवर सिस्टम के स्रोतों को संरक्षित करने की एक पहल है, क्योंकि वे महत्वपूर्ण सांस्कृतिक/वैज्ञानिक कलाकृतियां हैं। इसमें ऊपर उल्लिखित कई प्रणालियों के स्रोत हैं।
लोकप्रिय तकनीकें
- एकीकरण के साथ प्रथम क्रम संकल्प (कंप्यूटिंग)
- प्रतिरूप उन्मूलन
- विश्लेषणात्मक झांकी की विधि
- सुपरपोजिशन कैलकुलस एवं टर्म पुनर्लेखन
- प्रतिरूप परिक्षण
- गणितीय प्रेरण[20]
- बाइनरी निर्णय आरेख
- डीपीएलएल एल्गोरिदम
- एकीकरण (कंप्यूटिंग)#उच्च-क्रम एकीकरण|उच्च-क्रम एकीकरण
सॉफ्टवेयर सिस्टम
| 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 |
मुफ्त सॉफ्टवेयर
- ऑल्ट एर्गो
- स्वचालित
- सीवीसी (प्रमेय कहावत)
- ई प्रमेय समर्थक
- गोडेल मशीन
- ईसाप्लानर
- LCF (प्रमेय कहावत)
- मिज़ार प्रणाली
- एनयूपीआरएल
- विरोधाभास (प्रमेय कहावत)
- नीति9
- प्रोटोटाइप सत्यापन प्रणाली
- स्पार्क (प्रोग्रामिंग भाषा)
- बारह
- Z3 प्रमेय प्रोवर
मालिकाना सॉफ्टवेयर
यह भी देखें
- करी-हावर्ड पत्राचार
- प्रतीकात्मक गणना
- रामानुजन मशीन
- कंप्यूटर एडेड सबूत
- औपचारिक सत्यापन
- तर्क प्रोग्रामिंग
- सबूत की जाँच
- मॉडल जाँच
- सबूत जटिलता
- कंप्यूटर बीजगणित प्रणाली
- कार्यक्रम विश्लेषण (कंप्यूटर विज्ञान)
- सामान्य समस्या सॉल्वर
- औपचारिक गणित के लिए मेटामैथ भाषा
टिप्पणियाँ
- ↑ Frege, Gottlob (1879). शब्द लेखन. Verlag Louis Neuert.
- ↑ Frege, Gottlob (1884). अंकगणित की मूल बातें (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02.
- ↑ Bertrand Russell; Alfred North Whitehead (1910–1913). गणितीय सिद्धांत (1st ed.). Cambridge University Press.
- ↑ Bertrand Russell; Alfred North Whitehead (1927). गणितीय सिद्धांत (2nd ed.). Cambridge University Press.
- ↑ Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD). University of Paris.
- ↑ 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.0 7.1 7.2 7.3 Davis, Martin (2001). "The Early History of Automated Deduction". Robinson & Voronkov 2001.)
- ↑ Bibel, Wolfgang (2007). "प्रारंभिक इतिहास और स्वचालित कटौती के परिप्रेक्ष्य" (PDF). Ki 2007. LNAI. Springer (4667): 2–18. Archived (PDF) from the original on 2022-10-09. Retrieved 2 September 2012.
- ↑ 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.
- ↑ McCune, W.W. (1997). "रॉबिन्स समस्या का समाधान". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881. S2CID 30847540.
- ↑ Gina Kolata (December 10, 1996). "कंप्यूटर मैथ प्रूफ रीज़निंग पावर दिखाता है". The New York Times. Retrieved 2008-10-11.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ Kerber, Manfred. "How to prove higher order theorems in first order logic." (1999).
- ↑ 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.
- ↑ Sutcliffe, Geoff. "स्वचालित प्रमेय साबित करने के लिए टीपीटीपी समस्या पुस्तकालय". Retrieved 15 July 2019.
- ↑ "प्रमेय प्रोवर संग्रहालय". Michael Kohlhase. Retrieved 2022-11-20.
- ↑ Bundy, Alan (1999). गणितीय प्रेरण द्वारा प्रमाण का स्वचालन (PDF) (Technical report). Informatics Research Report. Vol. 2. Division of Informatics, University of Edinburgh. hdl:1842/3394.
संदर्भ
- Chang, Chin-Liang; Lee, Richard Char-Tung (2014) [1973]. Symbolic Logic and Mechanical Theorem Proving. Elsevier. ISBN 9780080917283.
- Loveland, Donald W. (2016) [1978]. Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science. Vol. 6. Elsevier. ISBN 9781483296777.
- Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer. ISBN 978-1461396871.
- Gallier, Jean H. (2015) [1986]. Logic for Computer Science: Foundations of Automatic Theorem Proving (2nd ed.). Dover. ISBN 978-0-486-78082-5.
This material may be reproduced for any educational purpose, ...
- Duffy, David A. (1991). Principles of Automated Theorem Proving. Wiley. ISBN 9780471927846.
- Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd ed.). McGraw–Hill. ISBN 9780079112514.
- Robinson, Alan; Voronkov, Andrei, eds. (2001). Handbook of Automated Reasoning. Vol. I. Elsevier, MIT Press. ISBN 9780080532790. II ISBN 9780262182232.
- Fitting, Melvin (2012) [1996]. First-Order Logic and Automated Theorem Proving (2nd ed.). Springer. ISBN 9781461223603.
