एसएलडी रिज़ॉल्यूशन

एसएलडी संकल्प ("चयनात्मक रैखिक निश्चित" खंड संकल्प) तर्क प्रोग्रामिंग में प्रयुक्त अनुमान का मूल नियम है। यह संकल्प (तर्क) का परिशोधन है, जो हॉर्न क्लॉज के लिए ध्वनि और खंडन पूर्णता (तर्क) दोनों है।

SLD अनुमान नियम

एक लक्ष्य खंड दिया गया है, जिसे हल करने के लिए किसी समस्या की उपेक्षा के रूप में दर्शाया गया है:

$\neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}$ चयनित शाब्दिक के साथ $\neg L_{i}$, और एक इनपुट निश्चित खंड:

$L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}$ जिसका सकारात्मक शाब्दिक (परमाणु) $L\,$ परमाणु के साथ एकीकरण (कंप्यूटिंग)। $L_{i}\,$ चयनित शाब्दिक का $\neg L_{i}\,$, SLD रिज़ॉल्यूशन एक अन्य लक्ष्य क्लॉज़ प्राप्त करता है, जिसमें चयनित शाब्दिक को इनपुट क्लॉज़ के नकारात्मक शाब्दिक और एकीकृत प्रतिस्थापन द्वारा प्रतिस्थापित किया जाता है $\theta \,$ लागू की गई है:

$(\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta$ सबसे सरल मामले में, प्रस्तावात्मक तर्क में, परमाणु $L_{i}\,$ और $L\,$ समान हैं, और एकीकृत प्रतिस्थापन $\theta \,$ खाली है। हालांकि, अधिक सामान्य मामले में, दो शाब्दिक समान बनाने के लिए एकीकृत प्रतिस्थापन आवश्यक है।

SLD नाम की उत्पत्ति

रॉबर्ट कोवाल्स्की द्वारा पेश किए गए अनाम अनुमान नियम के लिए मार्टेन वैन एम्डेन द्वारा एसएलडी संकल्प नाम दिया गया था। इसका नाम एसएल संकल्प से लिया गया है, जो तर्क के अप्रतिबंधित खंड रूप के लिए ध्वनि और खंडन दोनों पूर्ण है। SLD का मतलब निश्चित शर्तों के साथ SL रिज़ॉल्यूशन है।

एसएल और एसएलडी दोनों में, एल इस तथ्य के लिए खड़ा है कि संकल्प प्रमाण को खंडों के रैखिक अनुक्रम तक सीमित किया जा सकता है:

$C_{1},C_{2},\cdots ,C_{l}$ जहां शीर्ष खंड $C_{1}\,$ एक इनपुट क्लॉज है, और हर दूसरा क्लॉज $C_{i+1}\,$ एक संकल्पकर्ता है जिसके माता-पिता पिछले खंड हैं $C_{i}\,$. यदि अंतिम खंड है तो प्रमाण एक खंडन है $C_{l}\,$ खाली उपवाक्य है।

एसएलडी में, अनुक्रम में सभी खंड लक्ष्य खंड हैं, और अन्य माता-पिता एक इनपुट क्लॉज हैं। एसएल रिज़ॉल्यूशन में, अन्य माता-पिता या तो एक इनपुट क्लॉज या पूर्वज क्लॉज है जो पहले अनुक्रम में था।

एसएल और एसएलडी दोनों में, एस इस तथ्य के लिए खड़ा है कि किसी भी खंड में एकमात्र शाब्दिक हल किया गया है $C_{i}\,$ वह एक है जिसे चयन नियम या चयन फ़ंक्शन द्वारा विशिष्ट रूप से चुना जाता है। एसएल संकल्प में, चयनित शाब्दिक एक तक सीमित है जिसे हाल ही में खंड में पेश किया गया है। सबसे सरल मामले में, इस तरह के एक ढेर (सार डेटा प्रकार) | अंतिम-में-पहले-बाहर चयन फ़ंक्शन को उस क्रम से निर्दिष्ट किया जा सकता है जिसमें प्रोलॉग में अक्षर लिखे गए हैं। हालाँकि, SLD रिज़ॉल्यूशन में चयन फ़ंक्शन SL रिज़ॉल्यूशन और प्रोलॉग की तुलना में अधिक सामान्य है। चुने जा सकने वाले शाब्दिक पर कोई प्रतिबंध नहीं है।

एसएलडी रिज़ॉल्यूशन की कम्प्यूटेशनल व्याख्या

क्लॉसल लॉजिक में, एक एसएलडी खंडन दर्शाता है कि क्लॉज का इनपुट सेट असंतोषजनक है। तर्क प्रोग्रामिंग में, हालांकि, एक एसएलडी खंडन की एक कम्प्यूटेशनल व्याख्या भी है। शीर्ष उपवाक्य $\neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}$ उपलक्ष्यों के संयोजन के इनकार के रूप में व्याख्या की जा सकती है $L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}$. खंड की व्युत्पत्ति $C_{i+1}\,$ से $C_{i}\,$ एक लक्ष्य-घटाने की प्रक्रिया के रूप में एक इनपुट क्लॉज का उपयोग करके, उप-लक्ष्यों के एक नए सेट के पिछड़े तर्क के माध्यम से व्युत्पत्ति है। एकीकृत प्रतिस्थापन $\theta \,$ दोनों चयनित उप-लक्ष्य से प्रक्रिया के मुख्य भाग में इनपुट पास करते हैं और साथ ही साथ प्रक्रिया के शीर्ष से शेष अचयनित उप-लक्ष्यों तक आउटपुट पास करते हैं। खाली खंड केवल उपलक्ष्यों का एक खाली सेट है, जो संकेत करता है कि शीर्ष खंड में उपलक्ष्यों का प्रारंभिक संयोजन हल हो गया है।

SLD रिज़ॉल्यूशन रणनीतियाँ

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

एक पत्ता नोड, जिसमें कोई संतान नहीं है, एक सफल नोड है यदि इससे जुड़ा लक्ष्य खंड खाली खंड है। यह एक विफलता नोड है यदि इसका संबद्ध लक्ष्य खंड खाली नहीं है, लेकिन इसका चयनित शाब्दिक कार्यक्रम में निश्चित खंडों के सकारात्मक शाब्दिक के बिना एकीकृत होता है।

एसएलडी संकल्प इस अर्थ में गैर-नियतात्मक है कि यह खोज वृक्ष की खोज के लिए खोज रणनीति का निर्धारण नहीं करता है। प्रोलॉग पेड़ की गहराई-पहले, एक समय में एक शाखा की खोज करता है, बैकट्रैकिंग का उपयोग करते हुए जब यह विफलता नोड का सामना करता है। कंप्यूटिंग संसाधनों के उपयोग में गहराई-पहली खोज बहुत कुशल है, लेकिन अपूर्ण है यदि खोज स्थान में अनंत शाखाएँ हैं और खोज रणनीति इन्हें सीमित शाखाओं की प्राथमिकता में खोजती है: संगणना समाप्त नहीं होती है। चौड़ाई-प्रथम खोज|चौड़ाई-प्रथम, सर्वश्रेष्ठ-प्रथम खोज|सर्वश्रेष्ठ-प्रथम, और शाखा-और-बाध्य खोज सहित अन्य खोज रणनीतियाँ भी संभव हैं। इसके अलावा, खोज को क्रमिक रूप से, एक समय में एक नोड, या समानांतर में, कई नोड्स एक साथ किया जा सकता है।

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

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

उदाहरण

तर्क कार्यक्रम को देखते हुए: <वाक्यविन्यास लैंग = प्रोलॉग लाइन = 1> क्ष:- प. पी। </वाक्यविन्यास हाइलाइट>

और शीर्ष-स्तरीय लक्ष्य:

सिंटैक्सहाइलाइट लैंग = प्रोलॉग> क्यू। </वाक्यविन्यास हाइलाइट> खोज स्थान में एक ही शाखा होती है, जिसमें q तक घटा दिया जाता है p जो एक सफल संगणना का संकेत देते हुए, उप-लक्ष्यों के खाली सेट तक कम हो जाता है। इस मामले में, कार्यक्रम इतना सरल है कि चयन समारोह की कोई भूमिका नहीं है और किसी भी खोज की आवश्यकता नहीं है।

क्लॉज़ल लॉजिक में, प्रोग्राम को क्लॉज़ के सेट द्वारा दर्शाया जाता है:

$q\lor \neg p$

$p\,$ और शीर्ष-स्तरीय लक्ष्य को एक नकारात्मक शाब्दिक के साथ लक्ष्य खंड द्वारा दर्शाया गया है:

$\neg q$ खोज स्थान में एकल खंडन शामिल है:

$\neg q,\neg p,{\mathit {false}}$ कहाँ ${\mathit {false}}\,$ खाली खंड का प्रतिनिधित्व करता है।

यदि निम्नलिखित खंड कार्यक्रम में जोड़ा गया था:

q :- r.

तब खोज स्थान में एक अतिरिक्त शाखा होगी, जिसका पत्ता नोड r एक विफलता नोड है। प्रोलॉग में, यदि इस खंड को मूल कार्यक्रम के सामने जोड़ा गया था, तो प्रोलॉग उस क्रम का उपयोग करेगा जिसमें खोज स्थान की शाखाओं की जांच के क्रम को निर्धारित करने के लिए खंड लिखे गए हैं। प्रोलॉग पहले इस नई शाखा का प्रयास करेगा, असफल होगा, और फिर मूल कार्यक्रम की एकल शाखा की जांच करने और सफल होने के लिए पीछे हटेगा।

यदि खंड

p :- p.

अब प्रोग्राम में जोड़े गए हैं, तो सर्च ट्री में एक अनंत शाखा होगी। यदि इस क्लॉज को पहले आजमाया गया, तो प्रोलॉग एक अनंत लूप में चला जाएगा और सफल शाखा नहीं मिलेगी।

एसएलडीएनएफ

एसएलडीएनएफ विफलता के रूप में नकारात्मकता से निपटने के लिए एसएलडी संकल्प का विस्तार है। SLDNF में, लक्ष्य खंड में विफलता शाब्दिक के रूप में नकारात्मकता शामिल हो सकती है, जैसा कि प्रपत्र में कहा गया है $not(p)\,$, जिनका चयन केवल तभी किया जा सकता है जब उनमें कोई चर न हो। जब इस तरह के एक चर-मुक्त शाब्दिक का चयन किया जाता है, तो एक सबप्रूफ (या उप-संकलन) को यह निर्धारित करने का प्रयास किया जाता है कि क्या कोई एसएलडीएनएफ खंडन है जो संबंधित असंबद्ध शाब्दिक से शुरू होता है। $p\,$ शीर्ष खंड के रूप में। चयनित उपलक्ष्य $not(p)\,$ सबप्रूफ विफल होने पर सफल होता है, और यदि सबप्रूफ सफल होता है तो यह विफल हो जाता है।

यह भी देखें

• जॉन एलन रॉबिन्सन

संदर्भ

• Jean Gallier, SLD-Resolution and Logic Programming chapter 9 of Logic for Computer Science: Foundations of Automatic Theorem Proving, 2003 online revision (free to download), originally published by Wiley, 1986
• John C. Shepherdson, SLDNF-Resolution with Equality, Journal of Automated Reasoning 8: 297-306, 1992; defines semantics with respect to which SLDNF-resolution with equality is sound and complete

बाहरी संबंध

• [1] Definition from the Free On-Line Dictionary of Computing