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

From Vigyanwiki
No edit summary
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}}
स्वचालित प्रमेय प्रमाणित करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) [[स्वचालित तर्क]] एवं [[गणितीय तर्क]] का उपक्षेत्र है जो [[कंप्यूटर प्रोग्राम]] द्वारा [[गणितीय प्रमेय]] को प्रमाणित करने से संबंधित है। [[गणितीय प्रमाण]] पर स्वचालित तर्क [[कंप्यूटर विज्ञान]] के विकास के लिए प्रमुख प्रेरणा थी।
'''स्वचालित प्रमेय प्रमाणन''' करना (एटीपी या स्वचालित कटौती के रूप में भी जाना जाता है) [[स्वचालित तर्क]] एवं [[गणितीय तर्क]] का उपक्षेत्र है जो [[कंप्यूटर प्रोग्राम]] द्वारा [[गणितीय प्रमेय]] को प्रमाणन करने से संबंधित है। [[गणितीय प्रमाण]] पर स्वचालित तर्क [[कंप्यूटर विज्ञान]] के विकास के लिए प्रमुख प्रेरणा थी।


== तार्किक नींव ==
== तार्किक नींव ==
Line 15: Line 15:
== प्रथम कार्यान्वयन ==
== प्रथम कार्यान्वयन ==


[[द्वितीय विश्व युद्ध]] के पश्चात, प्रथम सामान्य प्रयोजन के कंप्यूटर उपलब्ध हो गए। 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 में [[ तर्क सिद्धांत मशीन ]]अधिक महत्वाकांक्षी थी, [[ एलन नेवेल ]], हर्बर्ट ए. साइमन एवं क्लिफ शॉ जे द्वारा विकसित प्रिन्सिपिया मैथेमेटिका के प्रस्तावात्मक तर्क के लिए  कटौती प्रणाली सी. शॉ. जॉनियाक पर भी चलने वाली, तर्क सिद्धांत मशीन ने प्रस्तावात्मक स्वयं सिद्धों के अल्प समुच्चय एवं तीन कटौती नियमों से प्रमाणों का निर्माण किया। [[मूड सेट करना|मूड समुच्चय करना]], (प्रस्तावात्मक) चर प्रतिस्थापन, एवं उनकी परिभाषा द्वारा सूत्रों का प्रतिस्थापन प्रणाली ने अनुमानी मार्गदर्शन का उपयोग किया, एवं प्रिन्सिपिया के पूर्व 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 में [[ तर्क सिद्धांत मशीन ]]अधिक महत्वाकांक्षी थी, [[ एलन नेवेल ]], हर्बर्ट ए. साइमन एवं क्लिफ शॉ जे द्वारा विकसित प्रिन्सिपिया मैथेमेटिका के प्रस्तावात्मक तर्क के लिए  कटौती प्रणाली सी. शॉ. जॉनियाक पर भी चलने वाली, तर्क सिद्धांत मशीन ने प्रस्तावात्मक स्वयं सिद्धों के अल्प समुच्चय एवं तीन कटौती नियमों से प्रमाणों का निर्माण किया। [[मूड सेट करना|मूड समुच्चय करना]], (प्रस्तावात्मक) चर प्रतिस्थापन, एवं उनकी परिभाषा द्वारा सूत्रों का प्रतिस्थापन प्रणाली ने अनुमानी मार्गदर्शन का उपयोग किया, एवं प्रिन्सिपिया के पूर्व 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>
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 के दशक के अंत में स्वचालित कटौती में अनुसंधान को वित्तपोषित करने वाली एजेंसियों ने व्यावहारिक अनुप्रयोगों की आवश्यकता पर बल देना प्रारम्भ किया। प्रथम फलदायी क्षेत्रों में से [[कार्यक्रम सत्यापन]] का था जिसके द्वारा पास्कल, एडा, आदि जैसी भाषाओं में कंप्यूटर प्रोग्राम की शुद्धता की पुष्टि करने की समस्या के लिए प्रथम-क्रम प्रमेय प्रवर्तकों को प्रारम्भ किया गया था। प्रारंभिक कार्यक्रम सत्यापन प्रणालियों में उल्लेखनीय स्टैनफोर्ड पास्कल सत्यापनकर्ता था। [[स्टैनफोर्ड विश्वविद्यालय]] में [[डेविड लकहम]] द्वारा विकसित<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> यह [[जॉन एलन रॉबिन्सन]] के [[संकल्प (तर्क)]] सिद्धांत का उपयोग करके स्टैनफोर्ड में विकसित स्टैनफोर्ड संकल्प कथन पर भी आधारित था। यह गणितीय समस्याओं का समाधान करने की क्षमता प्रदर्शित करने वाली प्रथम स्वचालित कटौती प्रणाली थी, जो समाधान औपचारिक रूप से प्रकाशित होने से पूर्व अमेरिकन मैथमैटिकल सोसाइटी के नोटिस में घोषित की गई थी।
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> यह [[जॉन एलन रॉबिन्सन]] के [[संकल्प (तर्क)]] सिद्धांत का उपयोग करके स्टैनफोर्ड में विकसित स्टैनफोर्ड संकल्प कथन पर भी आधारित था। यह गणितीय समस्याओं का समाधान करने की क्षमता प्रदर्शित करने वाली प्रथम स्वचालित कटौती प्रणाली थी, जो समाधान औपचारिक रूप से प्रकाशित होने से पूर्व अमेरिकन मैथमैटिकल सोसाइटी के नोटिस में घोषित की गई थी।


प्रथम-क्रम प्रमेय प्रमाणित करना स्वचालित प्रमेय प्रमाणित करने के सबसे परिपक्व उपक्षेत्रों में से है। तर्क पर्याप्त अभिव्यंजक है जो मनमाना समस्याओं के विनिर्देशन की अनुमति देता है, प्रायः यथोचित प्राकृतिक एवं सहज प्रविधि से दूसरी ओर, यह अभी भी अर्ध-निर्णायक है, एवं पूर्ण रूप से स्वचालित प्रणालियों को सक्षम करने के लिए कई ध्वनि एवं पूर्ण कैलकुली विकसित की गई हैं।<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 को (अन्य प्रणालियों के साथ) जोड़ा गया है जो r E-SETHEO प्रमाणि<nowiki/>त करता है।
* [[SETHEO]] लक्ष्य-निर्देशित [[ मॉडल उन्मूलन | प्रतिरूप उन्मूलन]] कलन पर आधारित उच्च-प्रदर्शन प्रणाली है, जिसे मूल रूप से वोल्फगैंग बिबेल के निर्देशन में समूह द्वारा विकसित किया गया है। समग्र प्रमेय में E एवं SETHEO को (अन्य प्रणालियों के साथ) जोड़ा गया है जो r E-SETHEO प्रमाणन<nowiki/> करता है।
* वैम्पायर प्रमेय कथन मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित एवं कार्यान्वित की गई थी। यह अब बढ़ती अंतरराष्ट्रीय समूह द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी प्रणाली प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के मध्य) विजयी किया है।
* वैम्पायर प्रमेय कथन मूल रूप से आंद्रेई वोरोंकोव एवं क्रिस्टोफ़ होडर द्वारा [[मैनचेस्टर विश्वविद्यालय]] में विकसित एवं कार्यान्वित की गई थी। यह अब बढ़ती अंतरराष्ट्रीय समूह द्वारा विकसित किया गया है। इसने 2001 से नियमित रूप से सीएडीई एटीपी प्रणाली प्रतियोगिता में एफओएफ डिवीजन (अन्य डिवीजनों के मध्य) विजयी किया है।
* वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए विशेष प्रणाली है। इसने निरंतर चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन विजयी किया है।
* वाल्डमिस्टर अर्निम बुच एवं थॉमस हिलेनब्रांड द्वारा विकसित यूनिट-इक्वेशनल फर्स्ट-ऑर्डर लॉजिक के लिए विशेष प्रणाली है। इसने निरंतर चौदह वर्षों (1997-2010) के लिए CASC UEQ डिवीजन विजयी किया है।
Line 107: Line 107:
| [[Vampire theorem prover|वेंपाइर]] ||[https://vprover.github.io/licence.html वैम्पायर लाइसेंस] ||  {{Yes|Via [[System on TPTP]]}} || {{Yes}} || {{Yes}} ||दिसम्बर 14, 2017
| [[Vampire theorem prover|वेंपाइर]] ||[https://vprover.github.io/licence.html वैम्पायर लाइसेंस] ||  {{Yes|Via [[System on TPTP]]}} || {{Yes}} || {{Yes}} ||दिसम्बर 14, 2017
|-
|-
| [[Theorem Proving System|प्रमेय प्रमाणित करने वाली प्रणाली (TPS)]] || [http://gtps.math.cmu.edu/cgi-bin/tpsdist.pl टीपीएस वितरण समझौता] || {{No}} || {{Yes}} || {{No}} ||फरवरी 4, 2012
| [[Theorem Proving System|प्रमेय प्रमाणन करने वाली प्रणाली (TPS)]] || [http://gtps.math.cmu.edu/cgi-bin/tpsdist.pl टीपीएस वितरण समझौता] || {{No}} || {{Yes}} || {{No}} ||फरवरी 4, 2012
|-
|-
| [[SPASS|एसपीए एस.एस]] || [[FreeBSD license|फ्रीबीएसडी लाइसेंस]] ||  {{Yes}}|| {{Yes}} ||  {{Yes}} ||नवंबर 2005
| [[SPASS|एसपीए एस.एस]] || [[FreeBSD license|फ्रीबीएसडी लाइसेंस]] ||  {{Yes}}|| {{Yes}} ||  {{Yes}} ||नवंबर 2005

Latest revision as of 16:14, 30 October 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] यह जॉन एलन रॉबिन्सन के संकल्प (तर्क) सिद्धांत का उपयोग करके स्टैनफोर्ड में विकसित स्टैनफोर्ड संकल्प कथन पर भी आधारित था। यह गणितीय समस्याओं का समाधान करने की क्षमता प्रदर्शित करने वाली प्रथम स्वचालित कटौती प्रणाली थी, जो समाधान औपचारिक रूप से प्रकाशित होने से पूर्व अमेरिकन मैथमैटिकल सोसाइटी के नोटिस में घोषित की गई थी।

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


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

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

कुछ महत्वपूर्ण प्रणालियाँ नीचे सूचीबद्ध हैं।

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

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

लोकप्रिय प्रविधियां

सॉफ्टवेयर प्रणाली

See also: प्रमाण सहायक §  तुलना, and [[:श्रेणी:प्रमेय सिद्ध करने वाले सॉफ़्टवेयर प्रणाली]]
तुलना
नाम लाइसेंस के प्रकार वेब सेवा पुस्तकालय स्टैंडअलोन अंतिम अपडेट (YYYY-mm-dd format)
ACL2 3-खंड बीएसडी No No Yes मई 2019
प्रोवेर 9/औटर पब्लिक डोमेन style="background:#9EFF9E;vertical-align:middle;text-align:center;" class="table-yes"|Via System on TPTP Yes No 2009
जैप जीपीएलv2 Yes Yes No 15 मई 2015
पी वी एस जीपीएल v2 No Yes No जनवरी 14, 2013
ईक्यूपी ? No Yes No मई 2009
फॉक्स ? No Yes No सितम्बर 28, 2017
कीमेरा जीपीएल style="background:#9EFF9E;vertical-align:middle;text-align:center;" class="table-yes"| Via Java Webstart Yes Yes 11 मार्च, 2015
इ जीपीएल Via System on TPTP No Yes जुलाई 4, 2017
स्नार्क Mozilla Public License 1.1 No Yes No 2012
वेंपाइर वैम्पायर लाइसेंस Via System on TPTP Yes Yes दिसम्बर 14, 2017
प्रमेय प्रमाणन करने वाली प्रणाली (TPS) टीपीएस वितरण समझौता No Yes No फरवरी 4, 2012
एसपीए एस.एस फ्रीबीएसडी लाइसेंस Yes Yes Yes नवंबर 2005
ईसाप्लानर GPL No Yes Yes 2007
की GPL Yes Yes Yes 11 अक्टूबर, 2017
Z3 प्रमेय प्रस्तावक एमआईटी लाइसेंस Yes Yes Yes नवम्बर 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=271683’