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

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