स्वचालित तर्क

From Vigyanwiki
Revision as of 14:12, 13 February 2023 by alpha>Indicwiki (Created page with "{{short description|Subfield of computer science and logic}} कंप्यूटर विज्ञान में, विशेष रूप से ज्ञान...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

कंप्यूटर विज्ञान में, विशेष रूप से ज्ञान प्रतिनिधित्व और तर्क और धातु विज्ञान में, स्वचालित तर्क का क्षेत्र तर्क के विभिन्न पहलुओं को समझने के लिए समर्पित है। स्वचालित तर्क का अध्ययन कंप्यूटर प्रोग्राम बनाने में मदद करता है जो कंप्यूटर को स्वचालित रूप से पूरी तरह से या लगभग पूरी तरह से तर्क करने की अनुमति देता है। यद्यपि स्वचालित तर्क को कृत्रिम बुद्धि का एक उप-क्षेत्र माना जाता है, इसका संबंध सैद्धांतिक कंप्यूटर विज्ञान और दर्शन से भी है।

स्वचालित तर्क के सबसे विकसित उपक्षेत्र स्वचालित प्रमेय साबित कर रहे हैं (और इंटरैक्टिव प्रमेय साबित करने के कम स्वचालित लेकिन अधिक व्यावहारिक उपक्षेत्र) और स्वचालित सबूत जांच (निश्चित मान्यताओं के तहत गारंटीकृत सही तर्क के रूप में देखा गया)।[citation needed] आगमनात्मक तर्क और अपवर्तक तर्क का उपयोग करते हुए सादृश्य द्वारा तर्क में व्यापक कार्य भी किया गया है।[1] अन्य महत्वपूर्ण विषयों में अनिश्चितता के तहत रीजनिंग और गैर-मोनोटोनिक तर्क|नॉन-मोनोटोनिक रीजनिंग शामिल हैं। अनिश्चितता क्षेत्र का एक महत्वपूर्ण हिस्सा तर्क का है, जहां अधिक मानक स्वचालित कटौती के शीर्ष पर न्यूनतमता और स्थिरता की बाधाओं को लागू किया जाता है। जॉन पोलक की ऑस्कर प्रणाली[2] एक स्वचालित तर्क प्रणाली का एक उदाहरण है जो केवल एक स्वचालित प्रमेय समर्थक होने की तुलना में अधिक विशिष्ट है।

स्वचालित तर्क के उपकरण और तकनीकों में शास्त्रीय तर्क्स और कैलकुली, फजी लॉजिक, बायेसियन अनुमान, अधिकतम एन्ट्रापी के सिद्धांत के साथ तर्क और कई कम औपचारिक तदर्थ तकनीक शामिल हैं।

प्रारंभिक वर्ष

औपचारिक तर्क के विकास ने स्वचालित तर्क के क्षेत्र में एक बड़ी भूमिका निभाई, जिससे स्वयं कृत्रिम बुद्धि का विकास हुआ। एक औपचारिक प्रमाण एक ऐसा प्रमाण है जिसमें प्रत्येक तार्किक निष्कर्ष को गणित के मौलिक स्वयंसिद्धों पर वापस जाँचा गया है। बिना किसी अपवाद के सभी मध्यवर्ती तार्किक चरणों की आपूर्ति की जाती है। अंतर्ज्ञान के लिए कोई अपील नहीं की जाती है, भले ही अंतर्ज्ञान से तर्क तक का अनुवाद नियमित हो। इस प्रकार, एक औपचारिक प्रमाण कम सहज और तार्किक त्रुटियों के लिए कम संवेदनशील होता है।[3] कुछ लोग 1957 की कॉर्नेल समर मीटिंग पर विचार करते हैं, जो कई तर्कशास्त्रियों और कंप्यूटर वैज्ञानिकों को एक साथ लाती है, स्वचालित तर्क या स्वचालित कटौती की उत्पत्ति के रूप में।[4] दूसरों का कहना है कि यह इससे पहले 1955 में नेवेल, शॉ और साइमन के तर्क सिद्धांतवादी कार्यक्रम के साथ शुरू हुआ था, या मार्टिन डेविस के 1954 में प्रेस्बर्गर अंकगणित के कार्यान्वयन के साथ। प्रेस्बर्गर की निर्णय प्रक्रिया (जिसने साबित किया कि दो सम संख्याओं का योग सम है)।[5] स्वचालित तर्क, हालांकि अनुसंधान का एक महत्वपूर्ण और लोकप्रिय क्षेत्र है, अस्सी और नब्बे के दशक की शुरुआत में एआई सर्दियों के माध्यम से चला गया। हालांकि, बाद में क्षेत्र को पुनर्जीवित किया गया। उदाहरण के लिए, 2005 में, Microsoft ने अपनी कई आंतरिक परियोजनाओं में सॉफ़्टवेयर सत्यापन का उपयोग करना शुरू कर दिया था और अपने 2012 के विज़ुअल सी संस्करण में एक तार्किक विनिर्देश और जाँच भाषा शामिल करने की योजना बना रहा है।[4]


महत्वपूर्ण योगदान

गणितीय सिद्धांत अल्फ्रेड नॉर्थ व्हाइटहेड और बर्ट्रेंड रसेल द्वारा लिखित औपचारिक तर्क में एक मील का पत्थर काम था। प्रिंसिपिया मैथेमेटिका - जिसका अर्थ गणित के सिद्धांत भी हैं - प्रतीकात्मक तर्क के संदर्भ में सभी या कुछ गणितीय अभिव्यक्तियों को प्राप्त करने के उद्देश्य से लिखा गया था। प्रिंसिपिया मैथेमेटिका को शुरू में 1910, 1912 और 1913 में तीन खंडों में प्रकाशित किया गया था।[6] लॉजिक थिओरिस्ट (एलटी) 1956 में एलन नेवेल, क्लिफ शॉ और हर्बर्ट ए. साइमन द्वारा प्रमेय सिद्ध करने में मानव तर्क की नकल करने के लिए विकसित किया गया पहला कार्यक्रम था और प्रिन्सिपिया मैथेमेटिका के अध्याय दो से बावन प्रमेयों पर प्रदर्शित किया गया था, जो अड़तीस को सिद्ध करता है। उनमें से।[7] प्रमेयों को सिद्ध करने के अलावा, कार्यक्रम में एक प्रमेय के लिए एक प्रमाण मिला जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमेय से अधिक सुरुचिपूर्ण था। अपने परिणामों को प्रकाशित करने के असफल प्रयास के बाद, नेवेल, शॉ और हर्बर्ट ने 1958 में अपने प्रकाशन द नेक्स्ट एडवांस इन ऑपरेशन रिसर्च में रिपोर्ट किया:

अब दुनिया में ऐसी मशीनें हैं जो सोचती हैं, सीखती हैं और सृजन करती हैं। इसके अलावा, इन चीजों को करने की उनकी क्षमता तब तक तेजी से बढ़ने जा रही है जब तक (भविष्य में) समस्याओं की सीमा जो वे संभाल सकते हैं, उस सीमा के साथ सह-विस्तृत हो जाएगी जिस पर मानव मन लागू किया गया है।[8] 'औपचारिक प्रमाण के उदाहरण'
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 HOL Light Harrison Henstock
2000 Fundamental- of Algebra Mizar Milewski Brynski
2000 Fundamental- of Algebra Coq Geuvers et al. Kneser
2004 Four Color Coq Gonthier Robertson et al.
2004 Prime Number Isabelle Avigad et al. Selberg-Erdős
2005 Jordan Curve HOL Light Hales Thomassen
2005 Brouwer Fixed Point HOL Light Harrison Kuhn
2006 Flyspeck 1 Isabelle Bauer- Nipkow Hales
2007 Cauchy Residue HOL Light Harrison Classical
2008 Prime Number HOL Light Harrison Analytic proof
2012 Feit-Thompson Coq Gonthier et al.[11] Bender, Glauberman and Peterfalvi
2016 Boolean Pythagorean triples problem Formalized as SAT Heule et al.[12] None


प्रूफ सिस्टम

बोयर-मूर प्रमेय प्रोवर (NQTHM)

Nqthm का डिज़ाइन जॉन मैक्कार्थी और वुडी ब्लेडोस से प्रभावित था। एडिनबर्ग, स्कॉटलैंड में 1971 में शुरू हुआ, यह प्योर लिस्प (प्रोग्रामिंग भाषा) का उपयोग करके बनाया गया एक पूरी तरह से स्वचालित प्रमेय प्रोवर था। NQTHM के मुख्य पहलू थे:
  1. कार्य तर्क के रूप में लिस्प का उपयोग।
  2. कुल पुनरावर्ती कार्यों के लिए परिभाषा के सिद्धांत पर निर्भरता।
# पुनर्लेखन और प्रतीकात्मक मूल्यांकन का व्यापक उपयोग।
  1. प्रतीकात्मक मूल्यांकन की विफलता पर आधारित एक प्रेरण अनुमानी।[13]
एचओएल लाइट
OCaml में लिखा गया, HOL लाइट को एक सरल और स्वच्छ तार्किक आधार और एक सुव्यवस्थित कार्यान्वयन के लिए डिज़ाइन किया गया है। शास्त्रीय उच्च क्रम तर्क के लिए यह अनिवार्य रूप से एक और सबूत सहायक है।[14]
कोक
फ्रांस में विकसित, Coq एक अन्य स्वचालित प्रूफ असिस्टेंट है, जो ऑब्जेक्टिव CAML या हास्केल (प्रोग्रामिंग भाषा) सोर्स कोड के रूप में विशिष्टताओं से स्वचालित रूप से निष्पादन योग्य प्रोग्राम निकाल सकता है। गुणों, कार्यक्रमों और प्रमाणों को उसी भाषा में औपचारिक रूप दिया जाता है जिसे इंडक्टिव कंस्ट्रक्शन (CIC) का कलन कहा जाता है।[15]


अनुप्रयोग

स्वचालित प्रमेय साबित करने के लिए स्वचालित तर्क का सबसे अधिक उपयोग किया जाता है। अक्सर, हालांकि, प्रमेय सिद्ध करने वालों को प्रभावी होने के लिए कुछ मानवीय मार्गदर्शन की आवश्यकता होती है और इसलिए आम तौर पर प्रमाण सहायक के रूप में अर्हता प्राप्त करते हैं। कुछ मामलों में ऐसे प्रमेयकर्ता प्रमेय को सिद्ध करने के लिए नए तरीके लेकर आए हैं। लॉजिक थिओरिस्ट इसका एक अच्छा उदाहरण है। यह कार्यक्रम प्रिंसिपिया मैथेमेटिका में एक प्रमेय के लिए एक प्रमाण के साथ आया जो व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमाण की तुलना में अधिक कुशल (कम चरणों की आवश्यकता) था। औपचारिक तर्क, गणित और कंप्यूटर विज्ञान, तर्क प्रोग्रामिंग, सॉफ्टवेयर और हार्डवेयर सत्यापन, सर्किट डिज़ाइन, और कई अन्य समस्याओं की बढ़ती संख्या को हल करने के लिए स्वचालित तर्क कार्यक्रम लागू किए जा रहे हैं। स्वचालित प्रमेय साबित करना (सटक्लिफ और सटनर 1998) ऐसी समस्याओं का एक पुस्तकालय है जिसे नियमित आधार पर अद्यतन किया जाता है। ऑटोमेटेड डिडक्शन कॉन्फ्रेंस (पेलेटियर, सटक्लिफ और सटनर 2002) पर सम्मेलन में नियमित रूप से आयोजित स्वचालित प्रमेय साबित करने वालों के बीच एक प्रतियोगिता भी होती है; प्रतियोगिता के लिए समस्याओं का चयन TPTP लाइब्रेरी से किया जाता है।[16]


यह भी देखें

सम्मेलन और कार्यशालाएं

पत्रिकाओं


समुदाय

संदर्भ

  1. ↑ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
  2. ↑ John L. Pollock
  3. ↑ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
  4. ↑ 4.0 4.1 "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
  5. ↑ 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
  6. ↑ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
  7. ↑ "The Logic Theorist and its Children". Retrieved 2010-10-18
  8. ↑ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  9. ↑ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, ISBN 9780521585330
  10. ↑ Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446, S2CID 14824949
  11. ↑ 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
  12. ↑ 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.
  13. ↑ The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23
  14. ↑ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
  15. ↑ Introduction to Coq. Retrieved 2010-10-23
  16. ↑ Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=स्वचालित_तर्क&oldid=87692’