तार्किक तर्क और प्रमेय सिद्ध करना

तार्किक तर्क और प्रमेय सिद्ध करना ज्ञान का प्रतिनिधित्व करने के लिए औपचारिक तर्क के उपयोग और कटौती के स्वचालन से संबंधित है, जिसमें निष्कर्षों को प्राप्त किया जाता है जो परिसर के एक समूह से आवश्यक रूप से निकलते हैं।

Definition

प्रमेय सिद्ध करना यह स्वचालित व्युत्पत्ति है कि क्या एक तार्किक सूत्र अभिगृहीतों के एक समूह से निकलता है, आमतौर पर लक्ष्य प्राप्त होने तक या विरोधाभास तक पहुँचने तक ध्वनि अनुमान नियमों के साथ सूत्रों में हेरफेर करके।

Scope

यह विषय प्रस्तावात्मक और प्रथम-क्रम तर्क में तर्क और इसे स्वचालित करने वाले एल्गोरिदम को शामिल करता है: प्रस्तावात्मक तर्क के लिए सत्य-तालिका और DPLL-आधारित संतोषजनक जाँच, प्रथम-क्रम तर्क के लिए एकीकरण और संकल्प सिद्धांत, आगे और पीछे की श्रृंखला, और तर्क प्रोग्रामिंग की नींव। यह अनुमान प्रक्रियाओं की सुदृढ़ता, पूर्णता और निर्णयक्षमता को संबोधित करता है। अनिश्चितता या चूक को सहन करने वाले तर्क को अनिश्चितता के तहत तर्क और गैर-एकदिष्ट तर्क पर संबंधित विषयों में माना जाता है।

Core questions

• किसी निष्कर्ष के लिए परिसर के एक समूह द्वारा निहित होने का क्या अर्थ है, और यांत्रिक रूप से निहितार्थ की जाँच कैसे की जाती है?
• संकल्प सिद्धांत, एकीकरण के साथ, प्रथम-क्रम तर्क के लिए एक एकल पूर्ण अनुमान नियम कैसे देता है?
• अनुमान रणनीतियों के रूप में आगे और पीछे की श्रृंखलाएँ कैसे भिन्न होती हैं?
• स्वचालित तर्क की सीमाएँ क्या हैं, यह देखते हुए कि प्रथम-क्रम वैधता केवल अर्ध-निर्णायक है?

Key concepts

• प्रस्तावात्मक और प्रथम-क्रम तर्क
• निहितार्थ और वैधता
• एकीकरण
• संकल्प और खंडन
• DPLL और SAT समाधान
• आगे और पीछे की श्रृंखला
• हॉर्न क्लॉज़ और तर्क प्रोग्रामिंग
• सुदृढ़ता और पूर्णता

Key theories

संकल्प सिद्धांत

रॉबिन्सन का संकल्प खंडों पर एक एकल अनुमान नियम है जो, एकीकरण के साथ संयुक्त होकर, प्रथम-क्रम तर्क के लिए खंडन-पूर्ण है: खंडों के किसी भी असंतोषजनक सेट को खाली खंड प्राप्त करके असंतोषजनक दिखाया जा सकता है।

DPLL और प्रस्तावात्मक संतोषजनक

डेविस-पुटनम प्रक्रिया और इसका DPLL शोधन इकाई प्रसार और शुद्ध-शाब्दिक उन्मूलन के साथ व्यवस्थित केस स्प्लिटिंग द्वारा प्रस्तावात्मक संतोषजनक का निर्णय करते हैं, जो आधुनिक SAT सॉल्वर का आधार बनते हैं।

तर्क प्रोग्रामिंग और पश्च-श्रृंखला

प्रथम-क्रम तर्क को हॉर्न क्लॉज़ तक सीमित करना और लक्ष्यों को पीछे की ओर हल करना तर्क प्रोग्रामिंग को जन्म देता है, जिसमें संगणना प्रमाण खोज है, जो एक तर्क विधि और एक प्रोग्रामिंग प्रतिमान दोनों प्रदान करता है।

Clinical relevance

स्वचालित प्रमेय सिद्ध करना और SAT/SMT समाधान का उपयोग हार्डवेयर और सॉफ्टवेयर सत्यापन, कार्यक्रम विश्लेषण, योजना और गणित में किया जाता है, जबकि प्रोलॉग जैसी तर्क प्रोग्रामिंग भाषाएँ डेटाबेस, पार्सिंग और नियम-आधारित प्रणालियों पर पश्च-श्रृंखला अनुमान लागू करती हैं।

History

गिलमोर, डेविस और पुटनम (1960) द्वारा प्रारंभिक प्रमाण प्रक्रियाओं ने प्रस्तावात्मक और मात्रात्मक तर्क को स्वचालित किया, और रॉबिन्सन के संकल्प सिद्धांत (1965) ने प्रथम-क्रम अनुमान को एक नियम में एकीकृत किया। 1970 के दशक में संकल्प को तर्क प्रोग्रामिंग और प्रोलॉग में परिष्कृत किया गया; SAT और SMT समाधान बाद में एक प्रमुख व्यावहारिक तकनीक के रूप में विकसित हुए।

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

संकल्प सिद्धांत क्या है?

संकल्प एक एकल अनुमान नियम है जो पूरक शाब्दिक वाले दो खंडों को लेता है और शेष को मिलाकर एक नया खंड उत्पन्न करता है। एकीकरण के साथ बार-बार लागू करने पर, यह दिखा सकता है कि प्रथम-क्रम खंडों का एक सेट असंतोषजनक है, जो खंडन द्वारा प्रमेयों को सिद्ध करने का आधार है।

क्या स्वचालित प्रमेय सिद्ध करने की समाप्ति की गारंटी है?

प्रस्तावात्मक तर्क के लिए, वैधता निर्णायक है, इसलिए प्रक्रियाएँ समाप्त हो जाती हैं। पूर्ण प्रथम-क्रम तर्क के लिए, वैधता केवल अर्ध-निर्णायक है: एक पूर्ण प्रमाणक अंततः किसी भी वैध सूत्र की पुष्टि करेगा, लेकिन एक अमान्य सूत्र पर हमेशा के लिए चल सकता है, इसलिए सामान्य तौर पर समाप्ति की गारंटी नहीं है।