स्वचालित तर्क संज्ञानात्मक विज्ञान का एक क्षेत्र है (जिसमें ज्ञान प्रतिनिधित्व और तर्क शामिल हैं) और तर्क के विभिन्न पहलुओं को समझने के लिए समर्पित मेटलोजिक है। स्वचालित तर्क का अध्ययन कंप्यूटर प्रोग्रामों का उत्पादन करने में मदद करता है जो कंप्यूटरों को पूरी तरह से या लगभग पूरी तरह से स्वचालित रूप से तर्क करने की अनुमति देते हैं। हालाँकि स्वचालित तर्क को कृत्रिम बुद्धिमत्ता का उप-क्षेत्र माना जाता है, लेकिन इसका सैद्धांतिक कंप्यूटर विज्ञान और दर्शन से भी संबंध है।
स्वचालित तर्क की सबसे विकसित उप-प्रजातियां स्वचालित प्रमेय साबित होती हैं (और इंटरएक्टिव प्रमेय साबित करने के लिए कम स्वचालित लेकिन अधिक व्यावहारिक सबफ़ील्ड) और स्वचालित प्रूफ जाँच (निश्चित मान्यताओं के तहत सही तर्क के रूप में गारंटी के रूप में देखी गई)। व्यापक काम भी किया गया है सादृश्य का उपयोग करके।
अन्य महत्वपूर्ण विषयों में अनिश्चितता और गैर-मोनोटोनिक तर्क के तहत तर्क शामिल हैं। अनिश्चितता क्षेत्र का एक महत्वपूर्ण हिस्सा तर्क का है, जहां अधिक मानक स्वचालित कटौती के शीर्ष पर न्यूनतमता और स्थिरता की बाधाओं को लागू किया जाता है। जॉन पोलक का OSCAR सिस्टम एक स्वचालित तर्क प्रणाली का एक उदाहरण है जो केवल एक स्वचालित सिद्धांतकार होने की तुलना में अधिक विशिष्ट है।
स्वचालित तर्क के उपकरण और तकनीकों में शास्त्रीय लॉजिक्स और केल्की, फ़ज़ी लॉजिक, बेइज़ियन अनुमान, मैक्सिमल एन्ट्रापी के साथ तर्क और कई कम औपचारिक तदर्थ तकनीक शामिल हैं।
शुरुआती वर्ष
औपचारिक तर्क के विकास ने स्वचालित तर्क के क्षेत्र में एक बड़ी भूमिका निभाई, जिसने खुद कृत्रिम बुद्धि का विकास किया। एक औपचारिक प्रमाण एक प्रमाण है जिसमें गणित के मौलिक स्वयंसिद्धों के प्रति प्रत्येक तार्किक अनुमान को जाँच लिया गया है। सभी मध्यवर्ती तार्किक चरणों को बिना किसी अपवाद के आपूर्ति की जाती है। अंतर्ज्ञान के लिए कोई अपील नहीं की जाती है, भले ही अंतर्ज्ञान से तर्क तक का अनुवाद नियमित हो। इस प्रकार, एक औपचारिक प्रमाण कम सहज है, और तार्किक त्रुटियों के लिए कम संवेदनशील है।
कुछ लोग 1957 की कॉर्नेल समर मीटिंग को मानते हैं, जो कई तर्कवादियों और कंप्यूटर वैज्ञानिकों को स्वचालित तर्क, या स्वचालित कटौती के मूल के रूप में एक साथ लाती है। अन्य लोगों का कहना है कि इससे पहले यह 1955 के लॉजिक न्यूर्ल, शॉ और साइमन के लॉजिक प्रोग्राम या मार्टिन डेविस की 1954 में प्रेस्बर्गर की निर्णय प्रक्रिया को लागू करने के साथ शुरू हुआ (जिसमें साबित हुआ कि दो सम संख्याओं का योग भी सम है) ।
स्वचालित तर्क, हालांकि अनुसंधान का एक महत्वपूर्ण और लोकप्रिय क्षेत्र, अस्सी और नब्बे के दशक के शुरुआती दिनों में "एआई सर्दियों" के माध्यम से चला गया। हालाँकि, बाद में इस क्षेत्र को पुनर्जीवित किया गया। उदाहरण के लिए, 2005 में, Microsoft ने अपनी कई आंतरिक परियोजनाओं में सत्यापन तकनीक का उपयोग करना शुरू कर दिया और अपने 2012 के विजुअल सी में एक तार्किक विनिर्देश और जाँच भाषा को शामिल करने की योजना बना रहा है।
महत्वपूर्ण योगदान
प्रिंसिपिया मैथेमेटिका अल्फ्रेड नॉर्थ व्हाइटहेड और बर्ट्रेंड रसेल द्वारा लिखित औपचारिक तर्क में एक मील का पत्थर का काम था। प्रिंसिपिया मैथेमेटिका - गणित के सिद्धांतों का भी अर्थ - प्रतीकात्मक तर्क के संदर्भ में सभी या कुछ गणितीय अभिव्यक्तियों को प्राप्त करने के उद्देश्य से लिखा गया था। प्रिंसिपिया मैथमेटिका को शुरू में 1910, 1912 और 1913 में तीन खंडों में प्रकाशित किया गया था।
लॉजिक थ्योरिस्ट (LT) 1956 में एलन नेवेल, क्लिफ शॉ और हर्बर्ट ए। साइमन द्वारा "मानव तर्क की नकल करने" के लिए प्रमेय सिद्ध करने के लिए विकसित किया गया था और प्रिंसिपिया मैथेमेटिका के अध्याय दो से बावन प्रमेयों पर प्रदर्शन किया गया था, ३८ साबित हुए। -उनमें से। प्रमेयों को सिद्ध करने के अलावा, कार्यक्रम में एक प्रमेय के लिए एक प्रमाण मिला, जो व्हाइटहेड और रसेल द्वारा प्रदान की गई तुलना में अधिक सुरुचिपूर्ण था। उनके परिणामों को प्रकाशित करने के असफल प्रयास के बाद, नेवेल, शॉ और हर्बर्ट ने 1958 में अपने प्रकाशन, द नेक्स्ट एडवांस इन ऑपरेशन रिसर्च:
"अब दुनिया में ऐसी मशीनें हैं जो सोचते हैं, सीखते हैं और बनाते हैं। इसके अलावा, इन चीजों को करने की उनकी क्षमता तब तक तेजी से बढ़ने वाली है (जब तक कि एक दृश्यमान भविष्य में) उनकी समस्याओं की सीमा सह-व्यापक नहीं होगी। वह सीमा जिस पर मानव मन लगाया गया है। "
अनुप्रयोग
स्वचालित प्रमेय का निर्माण करने के लिए स्वचालित तर्क का सबसे अधिक उपयोग किया जाता है। अक्सर, हालांकि, प्रमेय साबित करने के लिए कुछ मानव मार्गदर्शन की आवश्यकता होती है जो प्रभावी हो और इसलिए आमतौर पर प्रमाण सहायकों के रूप में योग्य होते हैं। कुछ मामलों में ऐसे प्रमेय एक प्रमेय साबित करने के लिए नए तरीकों के साथ आए हैं। लॉजिक थियोरिस्ट इसका एक अच्छा उदाहरण है। कार्यक्रम प्रिंसिपिया मैथेमेटिका में प्रमेयों में से एक के लिए एक प्रमाण के साथ आया था जो कि व्हाइटहेड और रसेल द्वारा प्रदान किए गए प्रमाण की तुलना में अधिक कुशल (कम चरणों की आवश्यकता) था। औपचारिक तर्क, गणित और कंप्यूटर विज्ञान, तर्क प्रोग्रामिंग, सॉफ्टवेयर और हार्डवेयर सत्यापन, सर्किट डिजाइन, और कई अन्य लोगों में समस्याओं की बढ़ती संख्या को हल करने के लिए स्वचालित तर्क कार्यक्रम लागू किए जा रहे हैं। TPTP (Sutcliffe और Suttner 1998) ऐसी समस्याओं का एक पुस्तकालय है जिसे नियमित आधार पर अपडेट किया जाता है। CADE सम्मेलन में नियमित रूप से आयोजित स्वचालित प्रमेय साबित करने वालों के बीच एक प्रतियोगिता भी है (पेल्लेटियर, सुटक्लिफ और सुटनर 2002); प्रतियोगिता के लिए समस्याओं को TPTP लाइब्रेरी से चुना गया है।
यह सभि देखे
- स्वचालित मशीन लर्निंग
- स्वचालित प्रमेय साबित करना
- रीजनिंग सिस्टम
- शब्दार्थ तार्किक
- कृत्रिम बुद्धि के अनुप्रयोग
- अनुमान इंजन