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

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

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

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

उदाहरण

तर्क कार्यक्रम को देखते हुए:

1 q :- p.
2 p.

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

q.

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

खंड तर्क में, प्रोग्राम को खण्ड़ के सेट द्वारा दर्शाया जाता है:

$q\lor \neg p$

$p\,$

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

$\neg q$

अन्वेषण स्थल में एकल खंडन सम्मलित है:

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

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

q :- r.

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

यदि खंड में

p :- p.

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

SLDNF

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