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

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

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 संकल्प से लिया गया है, जो तर्क के अप्रतिबंधित खंड रूप के लिए ध्वनि और खंडन दोनों पूर्ण है। SLD का अर्थ है निश्चित खंड के साथ SL एक विश्लेषण है।

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

$C_{1},C_{2},\cdots ,C_{l}$

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

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

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

SLD संकल्प की संगणनात्मक व्याख्या

खण्ड़ तर्क में, एक SLD खंडन दर्शाता है कि खण्ड़ का इनपुट सेट असंतोषजनक है। तर्क प्रोग्रामिंग में, चूंकि, एक SLD खंडन की एक संगणनात्मक व्याख्या भी है। शीर्ष उपवाक्य $\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 संकल्प स्पष्ट रूप से वैकल्पिक गणनाओं की एक अन्वेषण को परिभाषित करता है, जिसमें प्रारंभिक लक्ष्य खंड वृक्ष की जड़ से जुड़ा हुआ है। प्रत्येक निस्पंद के लिए और कार्यक्रम में प्रत्येक निश्चित खंड के लिए जिसका सकारात्मक शाब्दिक निस्पंद से जुड़े लक्ष्य खंड में चयनित शाब्दिक के साथ एकीकृत होता है, 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