स्वचालित तर्क: Difference between revisions
From Vigyanwiki
(Created page with "{{short description|Subfield of computer science and logic}} कंप्यूटर विज्ञान में, विशेष रूप से ज्ञान...") |
No edit summary |
||
| Line 2: | Line 2: | ||
[[कंप्यूटर विज्ञान]] में, विशेष रूप से [[ज्ञान प्रतिनिधित्व और तर्क]] और [[धातु विज्ञान]] में, स्वचालित तर्क का क्षेत्र तर्क के विभिन्न पहलुओं को समझने के लिए समर्पित है। स्वचालित तर्क का अध्ययन [[कंप्यूटर प्रोग्राम]] बनाने में मदद करता है जो कंप्यूटर को स्वचालित रूप से पूरी तरह से या लगभग पूरी तरह से तर्क करने की अनुमति देता है। यद्यपि स्वचालित तर्क को कृत्रिम बुद्धि का एक उप-क्षेत्र माना जाता है, इसका संबंध [[सैद्धांतिक कंप्यूटर विज्ञान]] और [[दर्शन]] से भी है। | [[कंप्यूटर विज्ञान]] में, विशेष रूप से [[ज्ञान प्रतिनिधित्व और तर्क]] और [[धातु विज्ञान]] में, स्वचालित तर्क का क्षेत्र तर्क के विभिन्न पहलुओं को समझने के लिए समर्पित है। स्वचालित तर्क का अध्ययन [[कंप्यूटर प्रोग्राम]] बनाने में मदद करता है जो कंप्यूटर को स्वचालित रूप से पूरी तरह से या लगभग पूरी तरह से तर्क करने की अनुमति देता है। यद्यपि स्वचालित तर्क को कृत्रिम बुद्धि का एक उप-क्षेत्र माना जाता है, इसका संबंध [[सैद्धांतिक कंप्यूटर विज्ञान]] और [[दर्शन]] से भी है। | ||
स्वचालित तर्क के सबसे विकसित उपक्षेत्र स्वचालित प्रमेय | स्वचालित तर्क के सबसे विकसित उपक्षेत्र स्वचालित प्रमेय प्रमाणित कर रहे हैं (और पारस्परिक प्रमेय प्रमाणित करने के कम स्वचालित लेकिन अधिक व्यावहारिक उपक्षेत्र) और स्वचालित प्रमाण जांच (निश्चित मान्यताओं के तहत गारंटीकृत सही तर्क के रूप में देखा गया)।{{citation needed|date=October 2019}} आगमनात्मक तर्क और अपवर्तक तर्क का उपयोग करते हुए सादृश्य द्वारा तर्क में व्यापक कार्य भी किया गया है।<ref>Defourneaux, Gilles, and Nicolas Peltier. "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.81.501&rep=rep1&type=pdf Analogy and abduction in automated deduction]." IJCAI (1). 1997.</ref> | ||
स्वचालित तर्क के उपकरण और तकनीकों में [[शास्त्रीय तर्क]] | अन्य महत्वपूर्ण विषयों में [[अनिश्चितता]] के तहत रीजनिंग और [[गैर-मोनोटोनिक तर्क]] नॉन-मोनोटोनिक रीजनिंग सम्मिलित हैं। अनिश्चितता क्षेत्र का एक महत्वपूर्ण भाग तर्क का है, जहां अधिक मानक स्वचालित कटौती के शीर्ष पर न्यूनतमता और स्थिरता की बाधाओं को लागू किया जाता है। जॉन पोलक की ऑस्कर प्रणाली<ref>[[John L. Pollock]]</ref> एक स्वचालित तर्क प्रणाली का एक उदाहरण है जो केवल एक स्वचालित प्रमेय समर्थक होने की तुलना में अधिक विशिष्ट है। | ||
स्वचालित तर्क के उपकरण और तकनीकों में [[शास्त्रीय तर्क]] और कैलकुली, [[फजी लॉजिक]], बायेसियन अनुमान, अधिकतम एन्ट्रापी के सिद्धांत के साथ तर्क और कई कम औपचारिक तदर्थ तकनीक सम्मिलित हैं। | |||
== प्रारंभिक वर्ष == | == प्रारंभिक वर्ष == | ||
[[औपचारिक तर्क]] के विकास ने स्वचालित तर्क के क्षेत्र में एक बड़ी भूमिका निभाई, जिससे स्वयं कृत्रिम बुद्धि का विकास हुआ। एक [[औपचारिक प्रमाण]] एक ऐसा प्रमाण है जिसमें प्रत्येक तार्किक निष्कर्ष को गणित के मौलिक स्वयंसिद्धों पर वापस जाँचा गया है। बिना किसी अपवाद के सभी मध्यवर्ती तार्किक चरणों की आपूर्ति की जाती है। अंतर्ज्ञान के लिए कोई अपील नहीं की जाती है, भले ही अंतर्ज्ञान से तर्क तक का अनुवाद नियमित हो। इस प्रकार, एक औपचारिक प्रमाण कम सहज और तार्किक त्रुटियों के लिए कम संवेदनशील होता है।<ref>C. Hales, Thomas [https://www.ams.org/notices/200811/tx081101370p.pdf "Formal Proof"], University of Pittsburgh. Retrieved on 2010-10-19</ref> | [[औपचारिक तर्क]] के विकास ने स्वचालित तर्क के क्षेत्र में एक बड़ी भूमिका निभाई, जिससे स्वयं कृत्रिम बुद्धि का विकास हुआ। एक [[औपचारिक प्रमाण]] एक ऐसा प्रमाण है जिसमें प्रत्येक तार्किक निष्कर्ष को गणित के मौलिक स्वयंसिद्धों पर वापस जाँचा गया है। बिना किसी अपवाद के सभी मध्यवर्ती तार्किक चरणों की आपूर्ति की जाती है। अंतर्ज्ञान के लिए कोई अपील नहीं की जाती है, भले ही अंतर्ज्ञान से तर्क तक का अनुवाद नियमित हो। इस प्रकार, एक औपचारिक प्रमाण कम सहज और तार्किक त्रुटियों के लिए कम संवेदनशील होता है।<ref>C. Hales, Thomas [https://www.ams.org/notices/200811/tx081101370p.pdf "Formal Proof"], University of Pittsburgh. Retrieved on 2010-10-19</ref> | ||
कुछ लोग 1957 की कॉर्नेल समर मीटिंग पर विचार करते हैं, जो कई तर्कशास्त्रियों और कंप्यूटर वैज्ञानिकों को एक साथ लाती है, स्वचालित तर्क या [[स्वचालित कटौती]] की उत्पत्ति के रूप | |||
स्वचालित तर्क, हालांकि अनुसंधान का एक महत्वपूर्ण और लोकप्रिय क्षेत्र है, अस्सी और नब्बे के दशक | कुछ लोग 1957 की कॉर्नेल समर मीटिंग पर विचार करते हैं, जो कई तर्कशास्त्रियों और कंप्यूटर वैज्ञानिकों को एक साथ लाती है, स्वचालित तर्क या [[स्वचालित कटौती]] की उत्पत्ति के रूप में<ref name="cornell">[http://www.cs.cornell.edu/info/projects/nuprl/Intro/AutoDeduction/autoded.html "Automated Deduction (AD)"], ''[The Nature of PRL Project]''. Retrieved on 2010-10-19</ref> दूसरों का कहना है कि यह इससे पहले 1955 में नेवेल, शॉ और साइमन के तर्क सिद्धांतवादी कार्यक्रम के साथ प्रारम्भ हुआ था, या मार्टिन डेविस के 1954 में प्रेस्बर्गर अंकगणित के कार्यान्वयन के साथ प्रेस्बर्गर की निर्णय प्रक्रिया (जिसने प्रमाणित किया कि दो सम संख्याओं का योग सम है) का कार्यान्वन हुआ।<ref>{{cite book | author=Martin Davis | contribution=The Prehistory and Early History of Automated Deduction | pages=1–28 | url=https://www.springer.com/gp/book/9783642819544 | isbn=978-3-642-81954-4 | editor1=Jörg Siekmann | editor2= G. Wrightson | title=Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966 | location=Heidelberg | publisher=Springer | year=1983 }} Here: p.15</ref> | ||
स्वचालित तर्क, हालांकि अनुसंधान का एक महत्वपूर्ण और लोकप्रिय क्षेत्र है, अस्सी और नब्बे के दशक के प्रारम्भ में एआई सर्दियों के माध्यम से चला गया। हालांकि, बाद में क्षेत्र को पुनर्जीवित किया गया। उदाहरण के लिए 2005 में, [[Microsoft|माइक्रोसॉफ्ट]] ने अपनी कई आंतरिक परियोजनाओं में सॉफ़्टवेयर सत्यापन का उपयोग करना प्रारम्भ कर दिया था और अपने 2012 के विज़ुअल सी संस्करण में एक तार्किक विनिर्देश और जाँच भाषा सम्मिलित करने की योजना बना रहा है।<ref name="cornell" /> | |||
== महत्वपूर्ण योगदान == | == महत्वपूर्ण योगदान == | ||
[[गणितीय सिद्धांत]] [[अल्फ्रेड नॉर्थ व्हाइटहेड]] और [[बर्ट्रेंड रसेल]] द्वारा लिखित औपचारिक तर्क में एक मील का पत्थर | [[गणितीय सिद्धांत]] [[अल्फ्रेड नॉर्थ व्हाइटहेड]] और [[बर्ट्रेंड रसेल]] द्वारा लिखित औपचारिक तर्क में एक मील का पत्थर प्रमुख था। प्रिंसिपिया मैथेमेटिका - जिसका अर्थ [[गणित के सिद्धांत]] भी हैं - [[प्रतीकात्मक तर्क]] के संदर्भ में सभी या कुछ [[गणितीय अभिव्यक्ति]]यों को प्राप्त करने के उद्देश्य से लिखा गया था। प्रिंसिपिया मैथेमेटिका को प्रारम्भ में 1910, 1912 और 1913 में तीन खंडों में प्रकाशित किया गया था।<ref>[http://plato.stanford.edu/entries/principia-mathematica/ "Principia Mathematica"], at [[Stanford University]]. Retrieved 2010-10-19</ref> | ||
लॉजिक थिओरिस्ट (एलटी) 1956 में [[एलन नेवेल]], [[क्लिफ शॉ]] और हर्बर्ट ए. साइमन द्वारा प्रमेय सिद्ध करने में मानव तर्क की नकल करने के लिए विकसित किया गया पहला कार्यक्रम था और प्रिन्सिपिया मैथेमेटिका के अध्याय दो से बावन प्रमेयों पर प्रदर्शित किया गया था, जो अड़तीस को सिद्ध करता है। उनमें से।<ref>[http://www.cs.swarthmore.edu/~eroberts/cs91/projects/ethics-of-ai/sec1_2.html "The Logic Theorist and its Children"]. Retrieved 2010-10-18</ref> प्रमेयों को सिद्ध करने के अलावा, कार्यक्रम में एक प्रमेय के लिए एक प्रमाण मिला जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमेय से अधिक सुरुचिपूर्ण था। अपने परिणामों को प्रकाशित करने के असफल प्रयास के बाद, नेवेल, शॉ और हर्बर्ट ने 1958 में अपने प्रकाशन द नेक्स्ट एडवांस इन ऑपरेशन रिसर्च में रिपोर्ट किया: | लॉजिक थिओरिस्ट (एलटी) 1956 में [[एलन नेवेल]], [[क्लिफ शॉ]] और हर्बर्ट ए. साइमन द्वारा प्रमेय सिद्ध करने में मानव तर्क की नकल करने के लिए विकसित किया गया पहला कार्यक्रम था और प्रिन्सिपिया मैथेमेटिका के अध्याय दो से बावन प्रमेयों पर प्रदर्शित किया गया था, जो अड़तीस को सिद्ध करता है। उनमें से।<ref>[http://www.cs.swarthmore.edu/~eroberts/cs91/projects/ethics-of-ai/sec1_2.html "The Logic Theorist and its Children"]. Retrieved 2010-10-18</ref> प्रमेयों को सिद्ध करने के अलावा, कार्यक्रम में एक प्रमेय के लिए एक प्रमाण मिला जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमेय से अधिक सुरुचिपूर्ण था। अपने परिणामों को प्रकाशित करने के असफल प्रयास के बाद, नेवेल, शॉ और हर्बर्ट ने 1958 में अपने प्रकाशन द नेक्स्ट एडवांस इन ऑपरेशन रिसर्च में रिपोर्ट किया: | ||
:: अब दुनिया में ऐसी मशीनें हैं जो सोचती हैं, सीखती हैं और सृजन करती हैं। इसके अलावा, इन चीजों को करने की उनकी क्षमता तब तक तेजी से बढ़ने जा रही है जब तक (भविष्य में) समस्याओं की सीमा जो वे संभाल सकते हैं, उस सीमा के साथ सह-विस्तृत हो जाएगी जिस पर मानव मन लागू किया गया है।<ref>Shankar, Natarajan ''[http://www.csl.sri.com/~shankar/ Little Engines of Proof]'', Computer Science Laboratory, [[SRI International]]. Retrieved 2010-10-19</ref> | :: अब दुनिया में ऐसी मशीनें हैं जो सोचती हैं, सीखती हैं और सृजन करती हैं। इसके अलावा, इन चीजों को करने की उनकी क्षमता तब तक तेजी से बढ़ने जा रही है जब तक (भविष्य में) समस्याओं की सीमा जो वे संभाल सकते हैं, उस सीमा के साथ सह-विस्तृत हो जाएगी जिस पर मानव मन लागू किया गया है।<ref>Shankar, Natarajan ''[http://www.csl.sri.com/~shankar/ Little Engines of Proof]'', Computer Science Laboratory, [[SRI International]]. Retrieved 2010-10-19</ref> | ||
:{| class="wikitable" | :'''<big>औपचारिक प्रमाण के उदाहरण</big>''' {| class="wikitable" |- ! Year !! Theorem !! Proof System !! Formalizer !! Traditional Proof |- | 1986 || [[Incompleteness theorem#First incompleteness theorem|First Incompleteness]]|| [[Boyer-Moore theorem prover|Boyer-Moore]] || Shankar<ref name="Shankar1994">{{Citation | last=Shankar | first=N. | title=Metamathematics, Machines, and Gödel's Proof | publisher=Cambridge University Press | place=Cambridge, UK | year=1994 | url=https://books.google.com/books?id=JmEXH9TllNcC | isbn=9780521585330 }}</ref> || [[Gödel]] |- | 1990 || [[Quadratic Reciprocity]] || [[Boyer-Moore theorem prover|Boyer-Moore]] || Russinoff<ref name="Russinoff1992">{{Citation | last=Russinoff | first=David M. | title=A Mechanical Proof of Quadratic Reciprocity | journal=J. Autom. Reason. | volume=8 | issue=1 | pages=3–21 | year=1992 | doi=10.1007/BF00263446 | s2cid=14824949 }}</ref> || [[Gotthold Eisenstein|Eisenstein]] |- | 1996 || [[Fundamental theorem of calculus|Fundamental- of Calculus]] || [[HOL Light|एचओएल Light]] || Harrison || Henstock |- | 2000 || [[Fundamental theorem of algebra|Fundamental- of Algebra]] || [[Mizar system|Mizar]] || Milewski || Brynski |- | 2000 || [[Fundamental theorem of algebra|Fundamental- of Algebra]] || [[Coq|कोक]] || Geuvers et al. || Kneser |- | 2004 || [[Four color theorem|Four Color]] || [[Coq|कोक]] || Gonthier || [[Neil Robertson (mathematician)|Robertson]] et al. |- | 2004 || [[Prime number theorem|Prime Number]] || [[Isabelle (proof assistant)|Isabelle]] || Avigad et al. || [[Atle Selberg|Selberg]]-[[Paul Erdős|Erdős]] |- | 2005 || [[Jordan curve theorem|Jordan Curve]] || [[HOL Light|एचओएल Light]] || Hales || Thomassen |- | 2005 || [[Brouwer fixed-point theorem|Brouwer Fixed Point]] || [[HOL Light|एचओएल Light]] || Harrison || Kuhn |- | 2006 || [[Kepler conjecture#A formal proof|Flyspeck 1]] || [[Isabelle (proof assistant)|Isabelle]] || Bauer- Nipkow || Hales |- | 2007 || [[Cauchy residue theorem|Cauchy Residue]] || [[HOL Light|एचओएल Light]] || Harrison || Classical |- | 2008 || [[Prime number theorem|Prime Number]] || [[HOL Light|एचओएल Light]] || Harrison || Analytic proof |- | 2012 || [[Feit-Thompson theorem|Feit-Thompson]] || [[Coq|कोक]] || Gonthier et al.<ref name="Gonthier2013">{{Citation | last1=Gonthier | first1=G. | last2=Asperti | first2=A. | display-authors=1 | chapter=A Machine-Checked Proof of the Odd Order Theorem | editor-last1=Blazy | editor-first1=S. | editor-last2=Paulin-Mohring | editor-first2=C. | editor-last3=Pichardie | editor-first3=D. | title=Interactive Theorem Proving | pages=163–179 | year=2013 | series=Lecture Notes in Computer Science | volume=7998 | doi=10.1007/978-3-642-39634-2_14 | isbn=978-3-642-39633-5 | s2cid=1855636 | chapter-url=http://www.cs.unibo.it/~asperti/PAPERS/odd_order.pdf }}</ref> || Bender, Glauberman and Peterfalvi |- | 2016 || [[Boolean Pythagorean triples problem]] || Formalized as [[Boolean satisfiability problem|SAT]] || Heule et al.<ref name="Heule2016">{{Cite book |arxiv = 1605.00723|doi = 10.1007/978-3-319-40970-2_15|chapter = Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer|title = Theory and Applications of Satisfiability Testing – SAT 2016|volume = 9710|pages = 228–245|series = Lecture Notes in Computer Science|year = 2016|author-link=Marijn Heule|last1 = Heule|first1 = Marijn J. H.|last2 = Kullmann|first2 = Oliver|last3 = Marek|first3 = Victor W.|isbn = 978-3-319-40969-6| s2cid=7912943 }}</ref> || None |} | ||
|- | |||
! Year !! Theorem !! Proof System !! Formalizer !! Traditional Proof | |||
|- | |||
| 1986 || [[Incompleteness theorem#First incompleteness theorem|First Incompleteness]]|| [[Boyer-Moore theorem prover|Boyer-Moore]] || Shankar<ref name="Shankar1994">{{Citation | last=Shankar | first=N. | title=Metamathematics, Machines, and Gödel's Proof | publisher=Cambridge University Press | place=Cambridge, UK | year=1994 | url=https://books.google.com/books?id=JmEXH9TllNcC | isbn=9780521585330 }}</ref> || [[Gödel]] | |||
|- | |||
| 1990 || [[Quadratic Reciprocity]] || [[Boyer-Moore theorem prover|Boyer-Moore]] || Russinoff<ref name="Russinoff1992">{{Citation | last=Russinoff | first=David M. | title=A Mechanical Proof of Quadratic Reciprocity | journal=J. Autom. Reason. | volume=8 | issue=1 | pages=3–21 | year=1992 | doi=10.1007/BF00263446 | s2cid=14824949 }}</ref> || [[Gotthold Eisenstein|Eisenstein]] | |||
|- | |||
| 1996 || [[Fundamental theorem of calculus|Fundamental- of Calculus]] || [[HOL Light]] || Harrison || Henstock | |||
|- | |||
| 2000 || [[Fundamental theorem of algebra|Fundamental- of Algebra]] || [[Mizar system|Mizar]] || Milewski || Brynski | |||
|- | |||
| 2000 || [[Fundamental theorem of algebra|Fundamental- of Algebra]] || [[Coq]] || Geuvers et al. || Kneser | |||
|- | |||
| 2004 || [[Four color theorem|Four Color]] || [[Coq]] || Gonthier || [[Neil Robertson (mathematician)|Robertson]] et al. | |||
|- | |||
| 2004 || [[Prime number theorem|Prime Number]] || [[Isabelle (proof assistant)|Isabelle]] || Avigad et al. || [[Atle Selberg|Selberg]]-[[Paul Erdős|Erdős]] | |||
|- | |||
| 2005 || [[Jordan curve theorem|Jordan Curve]] || [[HOL Light]] || Hales || Thomassen | |||
|- | |||
| 2005 || [[Brouwer fixed-point theorem|Brouwer Fixed Point]] || [[HOL Light]] || Harrison || Kuhn | |||
|- | |||
| 2006 || [[Kepler conjecture#A formal proof|Flyspeck 1]] || [[Isabelle (proof assistant)|Isabelle]] || Bauer- Nipkow || Hales | |||
|- | |||
| 2007 || [[Cauchy residue theorem|Cauchy Residue]] || [[HOL Light]] || Harrison || Classical | |||
|- | |||
| 2008 || [[Prime number theorem|Prime Number]] || [[HOL Light]] || Harrison || Analytic proof | |||
|- | |||
| 2012 || [[Feit-Thompson theorem|Feit-Thompson]] || [[Coq]] || Gonthier et al.<ref name="Gonthier2013">{{Citation | last1=Gonthier | first1=G. | last2=Asperti | first2=A. | display-authors=1 | chapter=A Machine-Checked Proof of the Odd Order Theorem | editor-last1=Blazy | editor-first1=S. | editor-last2=Paulin-Mohring | editor-first2=C. | editor-last3=Pichardie | editor-first3=D. | title=Interactive Theorem Proving | pages=163–179 | year=2013 | series=Lecture Notes in Computer Science | volume=7998 | doi=10.1007/978-3-642-39634-2_14 | isbn=978-3-642-39633-5 | s2cid=1855636 | chapter-url=http://www.cs.unibo.it/~asperti/PAPERS/odd_order.pdf }}</ref> || Bender, Glauberman and Peterfalvi | |||
|- | |||
| 2016 || [[Boolean Pythagorean triples problem]] || Formalized as [[Boolean satisfiability problem|SAT]] || Heule et al.<ref name="Heule2016">{{Cite book |arxiv = 1605.00723|doi = 10.1007/978-3-319-40970-2_15|chapter = Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer|title = Theory and Applications of Satisfiability Testing – SAT 2016|volume = 9710|pages = 228–245|series = Lecture Notes in Computer Science|year = 2016|author-link=Marijn Heule|last1 = Heule|first1 = Marijn J. H.|last2 = Kullmann|first2 = Oliver|last3 = Marek|first3 = Victor W.|isbn = 978-3-319-40969-6| s2cid=7912943 }}</ref> || None | |||
|} | |||
== | == प्रमाणित प्रणाली == | ||
बोयर-मूर प्रमेय प्रोवर ( | बोयर-मूर प्रमेय प्रोवर (एनक्यूटीएचएम) | ||
:[[Nqthm]] का डिज़ाइन जॉन मैक्कार्थी और वुडी ब्लेडोस से प्रभावित था। एडिनबर्ग, स्कॉटलैंड में 1971 में | :[[Nqthm|एनक्यूटीएचएम]] का डिज़ाइन जॉन मैक्कार्थी और वुडी ब्लेडोस से प्रभावित था। एडिनबर्ग, स्कॉटलैंड में 1971 में प्रारम्भ हुआ, यह प्योर [[लिस्प (प्रोग्रामिंग भाषा)]] का उपयोग करके बनाया गया एक पूरी तरह से स्वचालित प्रमेय प्रोवर था। एनक्यूटीएचएम के मुख्य पहलू थे: | ||
:# कार्य तर्क के रूप में लिस्प का उपयोग। | :# कार्य तर्क के रूप में लिस्प का उपयोग। | ||
:# कुल पुनरावर्ती कार्यों के लिए परिभाषा के सिद्धांत पर निर्भरता। | :# कुल पुनरावर्ती कार्यों के लिए परिभाषा के सिद्धांत पर निर्भरता। | ||
: # पुनर्लेखन और प्रतीकात्मक मूल्यांकन का व्यापक उपयोग। | :#पुनर्लेखन और प्रतीकात्मक मूल्यांकन का व्यापक उपयोग। | ||
:# प्रतीकात्मक मूल्यांकन की विफलता पर आधारित एक प्रेरण अनुमानी।<ref>''[http://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html The Boyer- Moore Theorem Prover]''. Retrieved on 2010-10-23</ref> | :#प्रतीकात्मक मूल्यांकन की विफलता पर आधारित एक प्रेरण अनुमानी।<ref>''[http://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html The Boyer- Moore Theorem Prover]''. Retrieved on 2010-10-23</ref> | ||
; [[एचओएल लाइट]] | ; [[एचओएल लाइट]] | ||
: [[OCaml]] में लिखा गया, | : [[OCaml|Oसीएएमएल]] में लिखा गया, एचओएल लाइट को एक सरल और स्वच्छ तार्किक आधार और एक सुव्यवस्थित कार्यान्वयन के लिए डिज़ाइन किया गया है। शास्त्रीय उच्च क्रम तर्क के लिए यह अनिवार्य रूप से एक और प्रमाण सहायक है।<ref>Harrison, John ''[http://www.cl.cam.ac.uk/~jrh13/slides/tphols-18aug09/slides.pdf HOL Light: an overview]''. Retrieved 2010-10-23</ref> | ||
; [[कोक]] | ; [[कोक]] | ||
: फ्रांस में विकसित, | : फ्रांस में विकसित, कोक एक अन्य स्वचालित प्रूफ असिस्टेंट है, जो ऑब्जेक्टिव सीएएमएल या [[हास्केल (प्रोग्रामिंग भाषा)]] सोर्स कोड के रूप में विशिष्टताओं से स्वचालित रूप से निष्पादन योग्य प्रोग्राम निकाल सकता है। गुणों, कार्यक्रमों और प्रमाणों को उसी भाषा में औपचारिक रूप दिया जाता है जिसे इंडक्टिव कंस्ट्रक्शन (सीआईसी) का कलन कहा जाता है।<ref>''[http://coq.inria.fr/a-short-introduction-to-coq Introduction to Coq]''. Retrieved 2010-10-23</ref> | ||
== अनुप्रयोग == | == अनुप्रयोग == | ||
स्वचालित प्रमेय | स्वचालित प्रमेय प्रमाणित करने के लिए स्वचालित तर्क का सबसे अधिक उपयोग किया जाता है। प्रायः, हालांकि, प्रमेय सिद्ध करने वालों को प्रभावी होने के लिए कुछ मानवीय मार्गदर्शन की आवश्यकता होती है और इसलिए सामान्यतः प्रमाण सहायक के रूप में अर्हता प्राप्त करते हैं। कुछ मामलों में ऐसे प्रमेयकर्ता प्रमेय को सिद्ध करने के लिए नए तरीके लेकर आए हैं। लॉजिक थिओरिस्ट इसका एक अच्छा उदाहरण है। यह कार्यक्रम प्रिंसिपिया मैथेमेटिका में एक प्रमेय के लिए एक प्रमाण के साथ आया जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमाण की तुलना में अधिक कुशल (कम चरणों की आवश्यकता) था। औपचारिक तर्क, गणित और कंप्यूटर विज्ञान, [[तर्क प्रोग्रामिंग]], सॉफ्टवेयर और हार्डवेयर सत्यापन, [[सर्किट डिज़ाइन|परिपथ डिज़ाइन]], और कई अन्य समस्याओं की बढ़ती संख्या को हल करने के लिए स्वचालित तर्क कार्यक्रम लागू किए जा रहे हैं। स्वचालित प्रमेय प्रमाणित करना (सटक्लिफ और सटनर 1998) ऐसी समस्याओं का एक पुस्तकालय है जिसे नियमित आधार पर अद्यतन किया जाता है। ऑटोमेटेड डिडक्शन कॉन्फ्रेंस (पेलेटियर, सटक्लिफ और सटनर 2002) पर फलन में नियमित रूप से आयोजित स्वचालित प्रमेय प्रमाणित करने वालों के बीच एक प्रतियोगिता भी होती है; प्रतियोगिता के लिए समस्याओं का चयन टीपीटीपी लाइब्रेरी से किया जाता है।<ref name="Stanford Encyclopedia">''[http://plato.stanford.edu/entries/reasoning-automated/ Automated Reasoning]'', [[Stanford Encyclopedia]]. Retrieved 2010-10-10</ref> | ||
== यह भी देखें == | == यह भी देखें == | ||
* [[स्वचालित मशीन लर्निंग]] (ऑटोएमएल) | * [[स्वचालित मशीन लर्निंग]] (ऑटोएमएल) | ||
* स्वचालित प्रमेय | * स्वचालित प्रमेय प्रमाणित करना | ||
* [[तर्क प्रणाली]] | * [[तर्क प्रणाली]] | ||
* [[शब्दार्थ तर्क करनेवाला]] | * [[शब्दार्थ तर्क करनेवाला]] | ||
| Line 84: | Line 58: | ||
* [[सामान्य ज्ञान तर्क]] | * [[सामान्य ज्ञान तर्क]] | ||
=== | ===फलन और कार्यशालाएं=== | ||
* [[स्वचालित तर्क पर अंतर्राष्ट्रीय संयुक्त सम्मेलन]] (IJCAR) | * [[स्वचालित तर्क पर अंतर्राष्ट्रीय संयुक्त सम्मेलन|स्वचालित तर्क पर अंतर्राष्ट्रीय संयुक्त फलन]] (IJCAR) | ||
* स्वचालित कटौती पर | * स्वचालित कटौती पर फलन (सीएडीई) | ||
* [[विश्लेषणात्मक झांकी और संबंधित विधियों के साथ स्वचालित तर्क पर अंतर्राष्ट्रीय सम्मेलन]] | * [[विश्लेषणात्मक झांकी और संबंधित विधियों के साथ स्वचालित तर्क पर अंतर्राष्ट्रीय सम्मेलन|विश्लेषणात्मक झांकी और संबंधित विधियों के साथ स्वचालित तर्क पर अंतर्राष्ट्रीय फलन]] | ||
===पत्रिकाओं=== | ===पत्रिकाओं=== | ||
* ''[[Journal of Automated Reasoning]]'' | * ''[[Journal of Automated Reasoning|स्वचालित तर्क का जर्नल]]'' | ||
Revision as of 23:24, 15 February 2023
कंप्यूटर विज्ञान में, विशेष रूप से ज्ञान प्रतिनिधित्व और तर्क और धातु विज्ञान में, स्वचालित तर्क का क्षेत्र तर्क के विभिन्न पहलुओं को समझने के लिए समर्पित है। स्वचालित तर्क का अध्ययन कंप्यूटर प्रोग्राम बनाने में मदद करता है जो कंप्यूटर को स्वचालित रूप से पूरी तरह से या लगभग पूरी तरह से तर्क करने की अनुमति देता है। यद्यपि स्वचालित तर्क को कृत्रिम बुद्धि का एक उप-क्षेत्र माना जाता है, इसका संबंध सैद्धांतिक कंप्यूटर विज्ञान और दर्शन से भी है।
स्वचालित तर्क के सबसे विकसित उपक्षेत्र स्वचालित प्रमेय प्रमाणित कर रहे हैं (और पारस्परिक प्रमेय प्रमाणित करने के कम स्वचालित लेकिन अधिक व्यावहारिक उपक्षेत्र) और स्वचालित प्रमाण जांच (निश्चित मान्यताओं के तहत गारंटीकृत सही तर्क के रूप में देखा गया)।[citation needed] आगमनात्मक तर्क और अपवर्तक तर्क का उपयोग करते हुए सादृश्य द्वारा तर्क में व्यापक कार्य भी किया गया है।[1]
अन्य महत्वपूर्ण विषयों में अनिश्चितता के तहत रीजनिंग और गैर-मोनोटोनिक तर्क नॉन-मोनोटोनिक रीजनिंग सम्मिलित हैं। अनिश्चितता क्षेत्र का एक महत्वपूर्ण भाग तर्क का है, जहां अधिक मानक स्वचालित कटौती के शीर्ष पर न्यूनतमता और स्थिरता की बाधाओं को लागू किया जाता है। जॉन पोलक की ऑस्कर प्रणाली[2] एक स्वचालित तर्क प्रणाली का एक उदाहरण है जो केवल एक स्वचालित प्रमेय समर्थक होने की तुलना में अधिक विशिष्ट है।
स्वचालित तर्क के उपकरण और तकनीकों में शास्त्रीय तर्क और कैलकुली, फजी लॉजिक, बायेसियन अनुमान, अधिकतम एन्ट्रापी के सिद्धांत के साथ तर्क और कई कम औपचारिक तदर्थ तकनीक सम्मिलित हैं।
प्रारंभिक वर्ष
औपचारिक तर्क के विकास ने स्वचालित तर्क के क्षेत्र में एक बड़ी भूमिका निभाई, जिससे स्वयं कृत्रिम बुद्धि का विकास हुआ। एक औपचारिक प्रमाण एक ऐसा प्रमाण है जिसमें प्रत्येक तार्किक निष्कर्ष को गणित के मौलिक स्वयंसिद्धों पर वापस जाँचा गया है। बिना किसी अपवाद के सभी मध्यवर्ती तार्किक चरणों की आपूर्ति की जाती है। अंतर्ज्ञान के लिए कोई अपील नहीं की जाती है, भले ही अंतर्ज्ञान से तर्क तक का अनुवाद नियमित हो। इस प्रकार, एक औपचारिक प्रमाण कम सहज और तार्किक त्रुटियों के लिए कम संवेदनशील होता है।[3]
कुछ लोग 1957 की कॉर्नेल समर मीटिंग पर विचार करते हैं, जो कई तर्कशास्त्रियों और कंप्यूटर वैज्ञानिकों को एक साथ लाती है, स्वचालित तर्क या स्वचालित कटौती की उत्पत्ति के रूप में[4] दूसरों का कहना है कि यह इससे पहले 1955 में नेवेल, शॉ और साइमन के तर्क सिद्धांतवादी कार्यक्रम के साथ प्रारम्भ हुआ था, या मार्टिन डेविस के 1954 में प्रेस्बर्गर अंकगणित के कार्यान्वयन के साथ प्रेस्बर्गर की निर्णय प्रक्रिया (जिसने प्रमाणित किया कि दो सम संख्याओं का योग सम है) का कार्यान्वन हुआ।[5]
स्वचालित तर्क, हालांकि अनुसंधान का एक महत्वपूर्ण और लोकप्रिय क्षेत्र है, अस्सी और नब्बे के दशक के प्रारम्भ में एआई सर्दियों के माध्यम से चला गया। हालांकि, बाद में क्षेत्र को पुनर्जीवित किया गया। उदाहरण के लिए 2005 में, माइक्रोसॉफ्ट ने अपनी कई आंतरिक परियोजनाओं में सॉफ़्टवेयर सत्यापन का उपयोग करना प्रारम्भ कर दिया था और अपने 2012 के विज़ुअल सी संस्करण में एक तार्किक विनिर्देश और जाँच भाषा सम्मिलित करने की योजना बना रहा है।[4]
महत्वपूर्ण योगदान
गणितीय सिद्धांत अल्फ्रेड नॉर्थ व्हाइटहेड और बर्ट्रेंड रसेल द्वारा लिखित औपचारिक तर्क में एक मील का पत्थर प्रमुख था। प्रिंसिपिया मैथेमेटिका - जिसका अर्थ गणित के सिद्धांत भी हैं - प्रतीकात्मक तर्क के संदर्भ में सभी या कुछ गणितीय अभिव्यक्तियों को प्राप्त करने के उद्देश्य से लिखा गया था। प्रिंसिपिया मैथेमेटिका को प्रारम्भ में 1910, 1912 और 1913 में तीन खंडों में प्रकाशित किया गया था।[6]
लॉजिक थिओरिस्ट (एलटी) 1956 में एलन नेवेल, क्लिफ शॉ और हर्बर्ट ए. साइमन द्वारा प्रमेय सिद्ध करने में मानव तर्क की नकल करने के लिए विकसित किया गया पहला कार्यक्रम था और प्रिन्सिपिया मैथेमेटिका के अध्याय दो से बावन प्रमेयों पर प्रदर्शित किया गया था, जो अड़तीस को सिद्ध करता है। उनमें से।[7] प्रमेयों को सिद्ध करने के अलावा, कार्यक्रम में एक प्रमेय के लिए एक प्रमाण मिला जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमेय से अधिक सुरुचिपूर्ण था। अपने परिणामों को प्रकाशित करने के असफल प्रयास के बाद, नेवेल, शॉ और हर्बर्ट ने 1958 में अपने प्रकाशन द नेक्स्ट एडवांस इन ऑपरेशन रिसर्च में रिपोर्ट किया:
- अब दुनिया में ऐसी मशीनें हैं जो सोचती हैं, सीखती हैं और सृजन करती हैं। इसके अलावा, इन चीजों को करने की उनकी क्षमता तब तक तेजी से बढ़ने जा रही है जब तक (भविष्य में) समस्याओं की सीमा जो वे संभाल सकते हैं, उस सीमा के साथ सह-विस्तृत हो जाएगी जिस पर मानव मन लागू किया गया है।[8]
- औपचारिक प्रमाण के उदाहरण {| class="wikitable" |- ! Year !! Theorem !! Proof System !! Formalizer !! Traditional Proof |- | 1986 || First Incompleteness|| Boyer-Moore || Shankar[9] || Gödel |- | 1990 || Quadratic Reciprocity || Boyer-Moore || Russinoff[10] || Eisenstein |- | 1996 || Fundamental- of Calculus || एचओएल Light || Harrison || Henstock |- | 2000 || Fundamental- of Algebra || Mizar || Milewski || Brynski |- | 2000 || Fundamental- of Algebra || कोक || Geuvers et al. || Kneser |- | 2004 || Four Color || कोक || Gonthier || Robertson et al. |- | 2004 || Prime Number || Isabelle || Avigad et al. || Selberg-Erdős |- | 2005 || Jordan Curve || एचओएल Light || Hales || Thomassen |- | 2005 || Brouwer Fixed Point || एचओएल Light || Harrison || Kuhn |- | 2006 || Flyspeck 1 || Isabelle || Bauer- Nipkow || Hales |- | 2007 || Cauchy Residue || एचओएल Light || Harrison || Classical |- | 2008 || Prime Number || एचओएल Light || Harrison || Analytic proof |- | 2012 || Feit-Thompson || कोक || Gonthier et al.[11] || Bender, Glauberman and Peterfalvi |- | 2016 || Boolean Pythagorean triples problem || Formalized as SAT || Heule et al.[12] || None |}
प्रमाणित प्रणाली
बोयर-मूर प्रमेय प्रोवर (एनक्यूटीएचएम)
- एनक्यूटीएचएम का डिज़ाइन जॉन मैक्कार्थी और वुडी ब्लेडोस से प्रभावित था। एडिनबर्ग, स्कॉटलैंड में 1971 में प्रारम्भ हुआ, यह प्योर लिस्प (प्रोग्रामिंग भाषा) का उपयोग करके बनाया गया एक पूरी तरह से स्वचालित प्रमेय प्रोवर था। एनक्यूटीएचएम के मुख्य पहलू थे:
- कार्य तर्क के रूप में लिस्प का उपयोग।
- कुल पुनरावर्ती कार्यों के लिए परिभाषा के सिद्धांत पर निर्भरता।
- पुनर्लेखन और प्रतीकात्मक मूल्यांकन का व्यापक उपयोग।
- प्रतीकात्मक मूल्यांकन की विफलता पर आधारित एक प्रेरण अनुमानी।[13]
- एचओएल लाइट
- Oसीएएमएल में लिखा गया, एचओएल लाइट को एक सरल और स्वच्छ तार्किक आधार और एक सुव्यवस्थित कार्यान्वयन के लिए डिज़ाइन किया गया है। शास्त्रीय उच्च क्रम तर्क के लिए यह अनिवार्य रूप से एक और प्रमाण सहायक है।[14]
- कोक
- फ्रांस में विकसित, कोक एक अन्य स्वचालित प्रूफ असिस्टेंट है, जो ऑब्जेक्टिव सीएएमएल या हास्केल (प्रोग्रामिंग भाषा) सोर्स कोड के रूप में विशिष्टताओं से स्वचालित रूप से निष्पादन योग्य प्रोग्राम निकाल सकता है। गुणों, कार्यक्रमों और प्रमाणों को उसी भाषा में औपचारिक रूप दिया जाता है जिसे इंडक्टिव कंस्ट्रक्शन (सीआईसी) का कलन कहा जाता है।[15]
अनुप्रयोग
स्वचालित प्रमेय प्रमाणित करने के लिए स्वचालित तर्क का सबसे अधिक उपयोग किया जाता है। प्रायः, हालांकि, प्रमेय सिद्ध करने वालों को प्रभावी होने के लिए कुछ मानवीय मार्गदर्शन की आवश्यकता होती है और इसलिए सामान्यतः प्रमाण सहायक के रूप में अर्हता प्राप्त करते हैं। कुछ मामलों में ऐसे प्रमेयकर्ता प्रमेय को सिद्ध करने के लिए नए तरीके लेकर आए हैं। लॉजिक थिओरिस्ट इसका एक अच्छा उदाहरण है। यह कार्यक्रम प्रिंसिपिया मैथेमेटिका में एक प्रमेय के लिए एक प्रमाण के साथ आया जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमाण की तुलना में अधिक कुशल (कम चरणों की आवश्यकता) था। औपचारिक तर्क, गणित और कंप्यूटर विज्ञान, तर्क प्रोग्रामिंग, सॉफ्टवेयर और हार्डवेयर सत्यापन, परिपथ डिज़ाइन, और कई अन्य समस्याओं की बढ़ती संख्या को हल करने के लिए स्वचालित तर्क कार्यक्रम लागू किए जा रहे हैं। स्वचालित प्रमेय प्रमाणित करना (सटक्लिफ और सटनर 1998) ऐसी समस्याओं का एक पुस्तकालय है जिसे नियमित आधार पर अद्यतन किया जाता है। ऑटोमेटेड डिडक्शन कॉन्फ्रेंस (पेलेटियर, सटक्लिफ और सटनर 2002) पर फलन में नियमित रूप से आयोजित स्वचालित प्रमेय प्रमाणित करने वालों के बीच एक प्रतियोगिता भी होती है; प्रतियोगिता के लिए समस्याओं का चयन टीपीटीपी लाइब्रेरी से किया जाता है।[16]
यह भी देखें
- स्वचालित मशीन लर्निंग (ऑटोएमएल)
- स्वचालित प्रमेय प्रमाणित करना
- तर्क प्रणाली
- शब्दार्थ तर्क करनेवाला
- कार्यक्रम विश्लेषण (कंप्यूटर विज्ञान)
- आर्टिफिशियल इंटेलिजेंस के अनुप्रयोग
- कृत्रिम बुद्धि की रूपरेखा
- कैस्युइस्ट्री • केस-आधारित रीज़निंग
- अपहरण का तर्क
- अनुमान इंजन
- सामान्य ज्ञान तर्क
फलन और कार्यशालाएं
- स्वचालित तर्क पर अंतर्राष्ट्रीय संयुक्त फलन (IJCAR)
- स्वचालित कटौती पर फलन (सीएडीई)
- विश्लेषणात्मक झांकी और संबंधित विधियों के साथ स्वचालित तर्क पर अंतर्राष्ट्रीय फलन
पत्रिकाओं
समुदाय
संदर्भ
- ↑ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
- ↑ John L. Pollock
- ↑ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
- ↑ 4.0 4.1 "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
- ↑ Martin Davis (1983). "The Prehistory and Early History of Automated Deduction". In Jörg Siekmann; G. Wrightson (eds.). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. pp. 1–28. ISBN 978-3-642-81954-4. Here: p.15
- ↑ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
- ↑ "The Logic Theorist and its Children". Retrieved 2010-10-18
- ↑ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
- ↑ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, ISBN 9780521585330
- ↑ Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446, S2CID 14824949
- ↑ Gonthier, G.; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem" (PDF), in Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (eds.), Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 7998, pp. 163–179, doi:10.1007/978-3-642-39634-2_14, ISBN 978-3-642-39633-5, S2CID 1855636
- ↑ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer". Theory and Applications of Satisfiability Testing – SAT 2016. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6. S2CID 7912943.
- ↑ The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23
- ↑ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
- ↑ Introduction to Coq. Retrieved 2010-10-23
- ↑ Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10
