स्थिर मॉडल शब्दार्थ

स्थिर मॉडल, या उत्तर समूह की अवधारणा का उपयोग तर्क प्रोग्रामिंग के लिए घोषणात्मक शब्दार्थ (कंप्यूटर विज्ञान) को परिभाषित करने के लिए किया जाता है, जिसमें अस्वीकृति विफलता के रूप में होती है। यह तर्क प्रोग्रामिंग में निषेध के अर्थ के साथ-साथ प्रोग्राम पूरा होने और अच्छी तरह से स्थापित शब्दार्थ के कई मानक दृष्टिकोणों में से एक है। स्थिर मॉडल शब्दार्थ उत्तर समूह प्रोग्रामिंग का आधार है ।

प्रेरणा

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

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ \operatorname {not} q.$

इस प्रोग्राम को देखते हुए, क्वेरी p सफल होंगे, क्योंकि प्रोग्राम में तथ्य के रूप में p सम्मलित हैं; क्वेरी q विफल हो जाएगा, क्योंकि यह किसी भी नियम के प्रमुख में नहीं होता है। क्वेरी r भी विफल हो जाएगा, क्योंकि मुख्य में r के साथ एकमात्र नियम में उसके शरीर में उपलक्ष्य q होता है  ; जैसा कि हमने देखा है, वह उपलक्ष्य विफल हो जाता है। अंत में, क्वेरी s सफल होता है, क्योंकि प्रत्येक उपलक्ष्य p, $\operatorname {not} q$ नहीं सफल होता है। (बाद वाला सफल होता है क्योंकि संबंधित सकारात्मक लक्ष्य q विफल रहता है।) संक्षेप में, दिए गए प्रोग्राम पर एसएलडीएनएफ संकल्प के व्यवहार को निम्नलिखित सत्य कार्य द्वारा दर्शाया जा सकता है:

p	q	r	s
T	F	F	T.

दूसरी ओर, दिए गए प्रोग्राम के नियमों को प्रस्ताव के सूत्रों के रूप में देखा जा सकता है यदि हम $\land$ संयोजन के साथ अल्पविराम की पहचान करते हैं , प्रतीक $\operatorname {not}$ निषेध $\neg$ के साथ और $F\leftarrow G$ को पीछे की ओर लिखे निहितार्थ $G\rightarrow F$ के रूप में मानने के लिए सहमत हैं। उदाहरण के लिए, दिए गए प्रोग्राम का अंतिम नियम, इस दृष्टिकोण से, प्रस्तावात्मक सूत्र के लिए वैकल्पिक संकेतन है

$p\land \neg q\rightarrow s.$

यदि हम ऊपर दिखाए गए सत्य कार्य के लिए प्रोग्राम के नियमों के सत्य मानों की गणना करते हैं तो हम देखेंगे कि प्रत्येक नियम को T मान मिलता है। दूसरे शब्दों में, वह कार्य प्रोग्राम का मॉडल सिद्धांत है। किन्तु इस प्रोग्राम के अन्य मॉडल भी हैं, उदाहरण के लिए

p	q	r	s
T	T	T	F.

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

नॉनमोनोटोनिक तर्क से संबंध

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

स्व-महामारी तर्क का सिंटैक्स मोडल ऑपरेटर का उपयोग करता है जो हमें सत्य और विश्वास के बीच अंतर करने की अनुमति देता है। माइकल गेलफॉन्ड [1987] ने पढ़ने का प्रस्ताव रखा नियम के शरीर में $\operatorname {not} p$ में $p$ को विश्वास नहीं किया जाता है और स्व-महामारी तर्क के संगत सूत्र के रूप में निषेध के साथ नियम को समझने के लिए। स्थिर मॉडल शब्दार्थ, अपने मूल रूप में, इस विचार के सुधार के रूप में देखा जा सकता है जो स्व-महामारी तर्क के स्पष्ट संदर्भों से बचा जाता है।

डिफ़ॉल्ट तर्क में एक डिफ़ॉल्ट अनुमान नियम के समान होता है, अतिरिक्त इसके कि इसके परिसर और निष्कर्ष के अतिरिक्त ,अतिरिक्त सूत्रों की सूची सम्मलित है जिसे औचित्य कहा जाता है। डिफ़ॉल्ट का उपयोग इस धारणा के अनुसार निष्कर्ष निकालने के लिए किया जा सकता है कि इसका औचित्य वर्तमान में जो माना जाता है उसके अनुरूप है। निकोल बिडोइट और क्रिस्टीन फ्रोइडेवॉक्स [1987] ने नियमों के निकायों में नकारात्मक परमाणुओं को औचित्य के रूप में मानने का प्रस्ताव दिया। उदाहरण के लिए नियम

$s\leftarrow p,\ \operatorname {not} q$

डिफ़ॉल्ट के रूप में समझा जा सकता है जो हमें $s$ से $p$ प्राप्त करने की अनुमति देता है ये मानते हुए कि $\neg q$ सुसंगत है। स्थिर मॉडल शब्दार्थ ही विचार का उपयोग करता है, किन्तु यह डिफ़ॉल्ट तर्क को स्पष्ट रूप से संदर्भित नहीं करता है।

स्थिर मॉडल

नीचे स्थिर मॉडल की परिभाषा, [गेलफॉन्ड और लाइफशिट्ज, 1988] से पुनरुत्पादित, दो सम्मेलनों का उपयोग करती है। सबसे पहले, सत्य कार्य को परमाणुओं के समूह के साथ पहचाना जाता है जो T मान प्राप्त करता है। उदाहरण के लिए, सत्य कार्य

p	q	r	s
T	F	F	T.

$\{p,s\}$ समूह से पहचाना जाता है । यह सम्मेलन हमें एक दूसरे के साथ सत्य कार्य की तुलना करने के लिए समूह समावेशन संबंध का उपयोग करने की अनुमति देता है। सभी सत्य समनुदेशनों में सबसे छोटा $\emptyset$ वह है जो प्रत्येक परमाणु को असत्य बनाता है; सबसे बड़ा सत्य कार्य प्रत्येक परमाणु को सत्य बनाता है।

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

$\operatorname {even} (0)\$

$\operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)$

इस प्रोग्राम में X मूल स्थितियाँ से बदलने के परिणाम के रूप में समझा जाता है

$0,\ s(0),\ s(s(0)),\dots .$

प्रत्येक संभव विधियों से परिणाम अनंत मूल प्रोग्राम है।

$\operatorname {even} (0)\$

$\operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)$

$\operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))$

$\dots$

परिभाषा

P को फॉर्म के नियमों का एक सेट होने दें

$A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

जहाँ $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ मूल परमाणु हैं। यदि P में निषेध नहीं है ($n=0$ प्रोग्राम के प्रत्येक नियम में) तो, परिभाषा के अनुसार, P का एकमात्र स्थिर मॉडल इसका मॉडल है जो समूह समावेशन के सापेक्ष न्यूनतम है। (निषेध के बिना किसी भी प्रोग्राम में बिल्कुल न्यूनतम मॉडल होता है।) इस परिभाषा को नकारात्मकता वाले प्रोग्राम के स्थितियों में विस्तारित करने के लिए, हमें निम्न रूप से परिभाषित संपादन की सहायक अवधारणा की आवश्यकता है।

जमीन के परमाणुओं के किसी भी समूह I के लिए , I के सापेक्ष P का अपचयन नियमों का वह समुच्चय है, जिससे निषेधन P प्राप्त नहीं होता है पहले प्रत्येक नियम को इस तरह गिराता है कि उसके शरीर में कम से कम एक परमाणु $C_{i}$ होता है।

$B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

I से संबंधित , और फिर शेष सभी नियमों के निकायों से भागों $\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$ को छोड़ना ।

हम कहते हैं I ,P का स्थिर मॉडल है यदि I , I के सापेक्ष P की कमी का स्थिर मॉडल है । (चूंकि संपादन में नकारात्मकता सम्मलित नहीं है, इसका स्थिर मॉडल पहले ही परिभाषित किया जा चुका है।) जैसा कि "स्थिर मॉडल" शब्द से पता चलता है, P का प्रत्येक स्थिर मॉडल P का मॉडल है ।

उदाहरण

इन परिभाषाओं को स्पष्ट करने के लिए, आइए हम इसकी जाँच करें $\{p,s\}$ प्रोग्राम का स्थिर मॉडल है

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ \operatorname {not} q.$

$\{p,s\}$ के सापेक्ष इस प्रोग्राम की कमी है

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p.$

(वास्तव में, चूंकि $q\not \in \{p,s\}$, भाग $\operatorname {not} q.\$को हटाकर प्रोग्राम से छूट प्राप्त की जाती है ) $\{p,s\}$ संपादन का स्थिर मॉडल है । (वास्तव में, परमाणुओं का यह समूह संपादन के प्रत्येक नियम को संतुष्ट करता है और इसमें समान संपत्ति के साथ कोई उचित उपसमुच्चय नहीं है।) इस प्रकार $\{p,s\}$ संपादन के स्थिर मॉडल की गणना करने के बाद हम उसी समूह पर पहुंचे। जिससे हमने प्रारंभिक की थी। परिणाम स्वरुप , वह समूह स्थिर मॉडल है।

अन्य 15 सेट में परमाणुओं $p,\ q,\ r,\ s$ से मिलकर उसी तरह जाँच करना दिखाता है कि इस प्रोग्राम का कोई अन्य स्थिर मॉडल नहीं है। उदाहरण के लिए, $\{p,q,r\}$ के सापेक्ष प्रोग्राम की कमी है

$p\$

$r\leftarrow p,\ q.$

$\{p\}$ संपादन का स्थिर मॉडल है , जो समूह $\{p,q,r\}$ से अलग है जिससे हमने प्रारंभिक की थी।

अद्वितीय स्थिर मॉडल के बिना प्रोग्राम

नकारात्मकता वाले प्रोग्राम में कई स्थिर मॉडल हो सकते हैं या कोई स्थिर मॉडल नहीं हो सकता है। उदाहरण के लिए, प्रोग्राम

$p\leftarrow \operatorname {not} q$

$q\leftarrow \operatorname {not} p$

दो स्थिर मॉडल $\{p\}$, $\{q\}$ हैं। नियम प्रोग्राम

$p\leftarrow \operatorname {not} p$

कोई स्थिर मॉडल नहीं है।

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

किन्तु उत्तर समूह प्रोग्रामिंग में स्थिर मॉडलों का उपयोग ऐसे प्रोग्राम पर अलग दृष्टिकोण प्रदान करता है। उस प्रोग्रामिंग प्रतिमान में, दी गई खोज समस्या तर्क प्रोग्राम द्वारा प्रस्तुत की जाती है जिससे कि प्रोग्राम के स्थिर मॉडल समाधान के अनुरूप हों। तब कई स्थिर मॉडल वाले प्रोग्राम कई समाधानों के साथ समस्याओं के अनुरूप होते हैं और बिना स्थिर मॉडल वाले प्रोग्राम अघुलनशील समस्याओं के अनुरूप होते हैं। उदाहरण के लिए, आठ रानियों की पहेली के 92 हल हैं; उत्तर समूह प्रोग्रामिंग का उपयोग करके इसे हल करने के लिए, हम इसे 92 स्थिर मॉडल वाले तर्क प्रोग्राम द्वारा एन्कोड करते हैं। इस दृष्टिकोण से, ठीक स्थिर मॉडल वाले तर्क प्रोग्राम उत्तर समूह प्रोग्रामिंग में विशेष होते हैं, जैसे बीजगणित में ठीक एक मूल वाले बहुपदों की तरह।

स्थिर मॉडल शब्दार्थ के गुण

इस खंड में, जैसा कि ऊपर स्थिर मॉडल की परिभाषा में है, एक तर्क प्रोग्राम से हमारा तात्पर्य प्रपत्र के नियमों के एक समूह से है

$A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

जहाँ $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ मूल परमाणु हैं।

प्रधान परमाणु: यदि परमाणु A तर्क प्रोग्राम P के स्थिर मॉडल से संबंधित है तब A,P के नियमों में से एक का प्रमुख है ।

न्यूनता: तर्क प्रोग्राम P का कोई भी स्थिर मॉडल समूह समावेशन के सापेक्ष P के मॉडलों में न्यूनतम है ।

एंटीचैन संपत्ति: यदि I और J उसी तर्क प्रोग्राम के स्थिर मॉडल हैं तो I , J का उचित उपसमुच्चय नहीं है । दूसरे शब्दों में, प्रोग्राम के स्थिर मॉडल का समूह एंटीचैन है।

एनपी-पूर्णता: यह परीक्षण करना कि परिमित ग्राउंड तर्क प्रोग्राम में स्थिर मॉडल है या नहीं, एनपी-पूर्ण है।

असफलता के रूप में निषेध के अन्य सिद्धांतों से संबंध

प्रोग्राम समापन

परिमित मूल प्रोग्राम का कोई भी स्थिर मॉडल न केवल प्रोग्राम का मॉडल है, बल्कि विफलता के रूप में इसकी नकारात्मकता का मॉडल भी है पूर्णता शब्दार्थ [मारेक और सुब्रह्मण्यन, 1989]। चूँकि, इसका विलोम सत्य नहीं है। उदाहरण के लिए, एक-नियम प्रोग्राम को पूरा करना

$p\leftarrow p$

टॉटोलॉजी (तर्क) $p\leftrightarrow p$ है । आदर्श $\emptyset$ इस पुनरुक्ति $p\leftarrow p$ का स्थिर मॉडल है , किन्तु इसका दूसरा मॉडल क्या $\{p\}\$ नहीं है। फ़्राँस्वा फेजेस [1994] ने तर्क प्रोग्राम पर वाक्यात्मक स्थिति पाई जो ऐसे प्रतिउदाहरणों को समाप्त करती है और प्रोग्राम के पूरा होने के प्रत्येक मॉडल की स्थिरता की गारंटी देती है। उसकी स्थिति को संतुष्ट करने वाले प्रोग्राम को तंग कहा जाता है।

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

अच्छी तरह से स्थापित शब्दार्थ

तर्क प्रोग्राम का सुस्थापित शब्दार्थ मॉडल सभी मूल परमाणुओं को तीन सेट में विभाजित करता है: सत्य, असत्य और अज्ञात। यदि परमाणु $P$ के सुस्थापित मॉडल में सत्य है तो यह $P$ के प्रत्येक स्थिर मॉडल के अंतर्गत आता है । सामान्यतः बातचीत पकड़ में नहीं आती है। उदाहरण के लिए, प्रोग्राम

$p\leftarrow \operatorname {not} q$

$q\leftarrow \operatorname {not} p$

$r\leftarrow p$

$r\leftarrow q$

$\{p,r\}$ और $\{q,r\}$ दो स्थिर मॉडल हैं। यदि $r$ उन दोनों का है, अच्छी तरह से स्थापित मॉडल में इसका मूल्य अज्ञात है।

इसके अतिरिक्त, यदि किसी प्रोग्राम के सुस्थापित मॉडल में कोई परमाणु झूठा है तो यह उसके किसी भी स्थिर मॉडल से संबंधित नहीं है। इस प्रकार तर्क प्रोग्राम का सुस्थापित मॉडल अपने स्थिर मॉडलों के प्रतिच्छेदन पर निचली सीमा और उनके संघ पर ऊपरी सीमा प्रदान करता है।

शक्तिशाली निषेध

अधूरी जानकारी का प्रतिनिधित्व

ज्ञान के प्रतिनिधित्व के दृष्टिकोण से, मूल परमाणुओं के समूह को ज्ञान की पूर्ण स्थिति के विवरण के रूप में माना जा सकता है। जो परमाणु समूह से संबंधित होते हैं उन्हें सत्य के रूप में जाना जाता है और जो परमाणु समूह से संबंधित नहीं होते हैं। झूठा जाना जाता है। ज्ञान की संभावित अपूर्ण स्थिति को सुसंगत किन्तु संभवतः अधूरे शाब्दिक समूह का उपयोग करके वर्णित किया जा सकता है, यदि परमाणु $p$ समूह से संबंधित नहीं है और इसकी अस्वीकृति समूह से संबंधित नहीं है तो यह ज्ञात नहीं है कि क्या $p$ सत्य है या असत्य।

तर्क प्रोग्रामिंग के संदर्भ में, यह विचार दो प्रकार के निषेध के बीच अंतर करने की आवश्यकता की ओर ले जाता है — विफलता के रूप में निषेध, ऊपर चर्चा की गई, और शक्तिशाली निषेध, जिसे यहां $\sim$ द्वारा दर्शाया गया है। निम्नलिखित उदाहरण, दो प्रकार के निषेध के बीच के अंतर को दर्शाता हुआ, जॉन मैककार्थी (कंप्यूटर वैज्ञानिक) का है। स्कूल बस रेलवे ट्रैक को इस अवस्था पर पार कर सकती है कि कोई ट्रेन नहीं आ रही है। यदि हमें जरूरी नहीं पता है कि कोई ट्रेन आ रही है या नहीं तो विफलता के रूप में निषेध का उपयोग करने वाला नियम

${\hbox{Cross}}\leftarrow {\hbox{not Train}}$

इस विचार का पर्याप्त प्रतिनिधित्व नहीं है: यह कहता है कि आने वाली ट्रेन के बारे में जानकारी के अभाव में पार करना ठीक है। शरीर में शक्तिशाली निषेध का उपयोग करने वाला कमजोर नियम श्रेष्ठतर है

${\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.$

यह कहता है कि यदि हमें पता है कि कोई ट्रेन नहीं आ रही है तो पार करना ठीक है।

सुसंगत स्थिर मॉडल

स्थिर मॉडलों के सिद्धांत में शक्तिशाली निषेध को सम्मलित करने के लिए, गेलफॉन्ड और लाइफशिट्ज [1991] ने प्रत्येक भाव $A$, $B_{i}$, $C_{i}$ को नियम में अनुमति दी

$A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

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

वैकल्पिक दृष्टिकोण [फेरारिस और लाइफशिट्ज, 2005] परमाणु के भागों के रूप में शक्तिशाली नकारात्मक व्यवहार करता है और इसे स्थिर मॉडल की परिभाषा में किसी भी बदलाव की आवश्यकता नहीं होती है। प्रबल निषेध के इस सिद्धांत में, हम दो प्रकार के परमाणुओं, सकारात्मक और नकारात्मक के बीच अंतर करते हैं और मानते हैं कि प्रत्येक नकारात्मक परमाणु $\sim A$ रूप की अभिव्यक्ति है , जहाँ $A\$ सकारात्मक परमाणु है। परमाणुओं के समूह को सुसंगत कहा जाता है यदि इसमें परमाणुओं के पूरक $\ A,\sim A$ जोड़े नहीं होते हैं । प्रोग्राम के सुसंगत स्थिर मॉडल [गेलफॉन्ड और लाइफशिट्ज, 1991] के अर्थ में इसके सुसंगत उत्तर समूह के समान हैं।

उदाहरण के लिए, प्रोग्राम

$p\leftarrow \operatorname {not} q$

$q\leftarrow \operatorname {not} p$

$r\$

$\sim r\leftarrow \operatorname {not} p$

$\{p,r\}\$ और $\ \{q,r,\sim r\}$ दो स्थिर मॉडल हैं। पहला मॉडल सुसंगत है, दूसरा नहीं है, क्योंकि इसमें दोनों परमाणु$\ r$ और परमाणु $\ \sim r$ हैं ।

बंद विश्व धारणा

[गेलफॉन्ड और लाइफशिट्ज, 1991] के अनुसार, विधेय के लिए बंद दुनिया की धारणा $p\$ नियम द्वारा व्यक्त किया जा सकता है

$\sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})$

(संबंध $p\$ टपल $X_{1},\dots ,X_{n}$ के लिए मान्य नहीं है यदि कोई प्रमाण नहीं है कि यह करता है)। उदाहरण के लिए, प्रोग्राम का स्थिर मॉडल

$p(a,b)\$

$p(c,d)\$

$\sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)$

2 सकारात्मक परमाणु होते हैं

$p(a,b),\ p(c,d)\$

और 14 नकारात्मक परमाणु

$\sim p(a,a),\ \sim p(a,c),\ \dots$

अर्थात,$p,\ a,\ b,\ c,\ d$ से बनने वाले अन्य सभी सकारात्मक मूल परमाणुओं का शक्तिशाली नकारात्मकता।

शक्तिशाली निषेध के साथ तर्क प्रोग्राम अपने कुछ विधेय के लिए बंद विश्व धारणा नियमों को सम्मलित कर सकता है और अन्य विधेय को खुली दुनिया की धारणा के क्षेत्र में छोड़ सकता है।

बाधाओं के साथ प्रोग्राम

ऊपर चर्चा किए गए पारंपरिक नियमों के संग्रह के अतिरिक्त कई प्रकार के तर्क प्रोग्राम के लिए स्थिर मॉडल शब्दार्थ को सामान्यीकृत किया गया है — फॉर्म के नियम

$A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

जहाँ $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ परमाणु हैं। साधारण विस्तार प्रोग्राम को बाधाओं को सम्मलित करने की अनुमति देता है — खाली मुख्य वाले नियम:

$\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.$

याद रखें कि यदि हम संयोजन के साथ अल्पविराम की पहचान करते हैं तो पारंपरिक नियम को प्रस्तावक सूत्र के लिए वैकल्पिक संकेतन $\land$ के रूप में देखा जा सकता है , प्रतीक $\operatorname {not}$ निषेध के साथ $\neg$ और इलाज के लिए सहमत हैं $F\leftarrow G$ निहितार्थ के रूप में $G\rightarrow F$ पीछे लिखा हुआ। इस परिपाटी को व्यवरोधों तक विस्तारित करने के लिए, हम व्यवरोध की पहचान उसके निकाय के संगत सूत्र के निषेधन से करते हैं:

$\neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).$

अब हम स्थिर मॉडल की परिभाषा को बाधाओं वाले प्रोग्राम तक बढ़ा सकते हैं। जैसा कि पारंपरिक प्रोग्राम के स्थितियों में होता है, हम उन प्रोग्राम से प्रारंभ करते हैं जिनमें नकारात्मकता नहीं होती है। ऐसा प्रोग्राम असंगत हो सकता है, तब हम कहते हैं कि इसका कोई स्थिर मॉडल नहीं है। यदि ऐसा कोई प्रोग्राम $P$ तब संगत है $P$ अद्वितीय न्यूनतम मॉडल है और उस मॉडल को एकमात्र स्थिर मॉडल $P$ माना जाता है ।

अगला, बाधाओं के साथ स्वैच्छिक प्रोग्राम के स्थिर मॉडल को पारंपरिक प्रोग्राम के स्थितियों में उसी तरह से बनाए गए कटौती का उपयोग करके परिभाषित किया गया है (ऊपर एक स्थिर मॉडल की परिभाषा देखें)।। समूह $I$ परमाणुओं का प्रोग्राम $P$ का स्थिर मॉडल है जिसमें बाधाएँ होती हैं यदि $I$ के सापेक्ष $P$ की कमी एक स्थिर मॉडल है और वह स्थिर मॉडल $I$ बराबर है ।

पारंपरिक प्रोग्राम के लिए ऊपर बताए गए स्थिर मॉडल शब्दार्थ के गुण बाधाओं की उपस्थिति में भी बने रहते हैं।

उत्तर समूह प्रोग्रामिंग में बाधाएँ महत्वपूर्ण भूमिका निभाती हैं क्योंकि तर्क प्रोग्राम $P$ में बाधाएँ जोड़ती हैं $P$ के स्थिर मॉडलों के संग्रह को प्रभावित करता है बहुत ही सरल विधियों से यह उन स्थिर मॉडलों को हटा देता है जो बाधा का उल्लंघन करते हैं। दूसरे शब्दों में, किसी भी प्रोग्राम के लिए $P$ बाधाओं और किसी भी बाधा $C$ के साथ , $P\cup \{C\}$ के स्थिर मॉडल $P$ के स्थिर मॉडल के रूप में चित्रित किया जा सकता है जो $C$ संतुष्ट करता है ।

वियोगात्मक प्रोग्राम

Main article: वियोगी डेटालॉग

वियोगात्मक नियम में, मुख्य कई परमाणुओं का संयोजन हो सकता है:

$A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$

(अर्धविराम को संयोजन के लिए वैकल्पिक अंकन $\lor$ के रूप में देखा जाता है )। पारंपरिक नियम इसके अनुरूप हैं $k=1$ और प्रोग्राम के लिए $k=0$ बाधाओं के साथ हैं। वियोगी प्रोग्राम [गेलफॉन्ड और लाइफशिट्ज 1991] के लिए स्थिर मॉडल शब्दार्थ का विस्तार करने के लिए, हम पहले परिभाषित करते हैं कि निषेध के अभाव में ($n=0$ प्रत्येक नियम में) किसी प्रोग्राम के स्थिर मॉडल उसके न्यूनतम मॉडल होते हैं। वियोगात्मक प्रोग्राम के लिए कटौती की परिभाषा बनी हुई है । समूह $I$ परमाणुओं $P$ का स्थिर मॉडल है यदि $I$ , $P$ के सापेक्ष $I$ की कमी का स्थिर मॉडल है.

उदाहरण के लिए, समूह $\{p,r\}$ विघटनकारी प्रोग्राम का स्थिर मॉडल है

$p;q\$

$r\leftarrow \operatorname {not} q$

क्योंकि यह संपादन के दो न्यूनतम मॉडलों में एक से है

$p;q\$

$r.\$

उपरोक्त प्रोग्राम में एक और स्थिर मॉडल $\{q\}$ है।

जैसा कि पारंपरिक प्रोग्राम के स्थितियों में होता है, वियोजनात्मक प्रोग्राम के किसी भी स्थिर मॉडल $P$ का प्रत्येक तत्व का मुख्य परमाणु$P$ है , इस अर्थ में कि यह नियमों में से $P$ के प्रमुख में होता है । जैसा कि पारंपरिक स्थितियों में, वियोगात्मक प्रोग्राम के स्थिर मॉडल न्यूनतम होते हैं और एंटीचैन बनाते हैं। परिमित वियोजन कार्यक्रम में एक स्थिर मॉडल है या नहीं इसका परीक्षण करना $\Sigma _{2}^{\rm {P}}$-पूर्ण [ईटर और गोटलॉब, 1993] है।

प्रस्तावात्मक सूत्रों के समूह के स्थिर मॉडल

नियम और यहां तक ​​​​कि वियोगात्मक प्रोग्राम , स्वच्छंद प्रस्तावक सूत्रों की तुलना में विशेष वाक्यात्मक रूप है। प्रत्येक वियोगात्मक नियम अनिवार्य रूप से एक निहितार्थ है जैसे कि इसका पूर्ववर्ती (नियम का शरीर) शाब्दिक संयोजन है और इसका परिणामी (सिर) परमाणुओं का संयोजन है। डेविड पियर्स [1997] और पाओलो फेरारिस [2005] ने दिखाया कि कैसे स्थिर मॉडल की परिभाषा को स्वैच्छिक प्रस्तावात्मक सूत्रों के समूह तक बढ़ाया जाए। इस सामान्यीकरण में उत्तर समूह प्रोग्रामिंग के अनुप्रयोग हैं।

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

स्थिर मॉडल की सामान्य परिभाषा

[फेरारिस, 2005] के अनुसार, प्रस्तावक सूत्र $F$ की कमी समूह $I$ के सापेक्ष परमाणुओं से प्राप्त सूत्र $F$ है प्रत्येक $I$ अधिकतम उपसूत्र को प्रतिस्थापित करके जो संतुष्ट नहीं है तार्किक स्थिरांक के साथ $\bot$ (असत्य)। समूह $P$ की कमी $I$ के सापेक्ष प्रस्तावक सूत्र $I$ के सापेक्ष $P$ से सभी सूत्रों की कटौती सम्मलित है। जैसा कि विघटनकारी प्रोग्राम के स्थितियों में, हम कहते हैं कि समूह $I$ परमाणुओं का स्थिर मॉडल$P$ है यदि $I$ , $I$ के सापेक्ष $P$ कम करने के मॉडल के बीच न्यूनतम (समूह समावेशन के संबंध में) है ।

उदाहरण के लिए, समूह की कमी

$\{p,\ p\land q\rightarrow r,\ p\land \neg q\rightarrow s\}$

$\{p,s\}$ के सापेक्ष है

$\{p,\ \bot \rightarrow \bot ,\ p\land \neg \bot \rightarrow s\}.$

तब से $\{p,s\}$ संपादन का मॉडल है और उस समूह $\{p,s\}$ के उचित उपसमुच्चय संपादन के मॉडल नहीं हैं, सूत्रों के दिए गए समूह का स्थिर मॉडल है।

हमने देखा है कि $\{p,s\}$ भी उसी सूत्र का एक स्थिर मॉडल है, परिभाषा के अर्थ में तर्क प्रोग्रामिंग संकेत चिन्ह में लिखे गए उसी सूत्र का स्थिर मॉडल भी है। यह सामान्य तथ्य का उदाहरण है: पारंपरिक नियमों के समूह (सूत्रों के अनुरूप) के आवेदन में, फेरारीस के अनुसार स्थिर मॉडल की परिभाषा मूल परिभाषा के बराबर है। अधिक सामान्यतः बाध्यता और वियोगात्मक प्रोग्राम वाले प्रोग्राम के लिए वही सच है।

सामान्य स्थिर मॉडल शब्दार्थ के गुण

प्रमेय यह प्रमाणित करता है कि किसी प्रोग्राम के किसी भी स्थिर मॉडल $P$ के सभी तत्व $P$ के प्रमुख परमाणु हैं प्रस्तावित सूत्रों के समूह तक बढ़ाया जा सकता है, यदि हम मुख्य के परमाणुओं को निम्नानुसार परिभाषित करते हैं। परमाणु $A$ समूह का $P$प्रमुख परमाणु है प्रस्तावित सूत्रों की कम से कम घटना यदि $A$ से सूत्र में $P$ न तो निषेध के क्षेत्र में है और न ही निहितार्थ के पूर्ववर्ती में है। (हम यहाँ मानते हैं कि तुल्यता को एक संक्षिप्त नाम के रूप में माना जाता है न कि मौलिक संयोजक के रूप में।)

पारंपरिक प्रोग्राम के स्थिर मॉडल शब्दार्थ के गुण सामान्य स्थितियों में नहीं होते हैं। उदाहरण के लिए, (सिंगलटन समूह जिसमें सम्मलित है) सूत्र

$p\lor \neg p$

दो स्थिर मॉडल $\emptyset$ और $\{p\}$ हैं। उत्तरार्द्ध न्यूनतम नहीं है और यह पूर्व का उचित समूह है।

$\Sigma _{2}^{\rm {P}}$ -पूर्ण है, जैसा कि वियोगात्मक प्रोग्राम के स्थितियों में है, यह जांचना कि क्या प्रस्तावपरक सूत्रों के परिमित समूह का एक स्थिर मॉडल है।

यह भी देखें

• उत्तर समूह प्रोग्रामिंग
• तर्क प्रोग्रामिंग
• असफलता के रूप में नकारात्मकता

संदर्भ

• Bidoit, N.; Froidevaux, C. (1987). "Minimalism subsumes default logic and circumscription". Proceedings: Symposium on Logic in Computer Science, Ithaca, New York, June 22-25, 1987. IEEE Computer Society Press. pp. 89–97. ISBN 978-0-8186-0793-6. 87CH2464-6.
• Eiter, T.; Gottlob, G. (1993). "Complexity results for disjunctive logic programming and application to nonmonotonic logics". ILPS '93: Proceedings of the 1993 international symposium on Logic programming. MIT Press. pp. 266–278. ISBN 978-0-262-63152-5.
• van Emden, M.; Kowalski, R. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991. S2CID 11048276.
• Fages, F. (1994). "Consistency of Clark's completion and existence of stable models". Journal of Methods of Logic in Computer Science. 1: 51–60. CiteSeerX 10.1.1.48.2157.
• Ferraris, P. (2005). "Answer sets for propositional theories". Logic Programming and Nonmonotonic Reasoning. LPNMR 2005. Lecture Notes in Computer Science. Vol. 3662. Springer. pp. 119–131. CiteSeerX 10.1.1.129.5332. doi:10.1007/11546207_10. ISBN 978-3-540-31827-9.
• Ferraris, P.; Lifschitz, V. (2005). "Mathematical foundations of answer set programming". We Will Show Them! Essays in Honour of Dov Gabbay. King's College Publications. pp. 615–664. CiteSeerX 10.1.1.79.7622.
• Gelfond, M. (1987). "On stratified autoepistemic theories" (PDF). AAAI'87: Proceedings of the sixth National conference on Artificial intelligence. pp. 207–211. ISBN 978-0-934613-42-2.
• Gelfond, M.; Lifschitz, V. (1988). "The stable model semantics for logic programming". Proceedings of the Fifth International Conference on Logic Programming (ICLP). MIT Press. pp. 1070–80. ISBN 978-0-262-61054-4.
• Gelfond, M.; Lifschitz, V. (1991). "Classical negation in logic programs and disjunctive databases". New Generation Computing. 9 (3–4): 365–385. CiteSeerX 10.1.1.49.9332. doi:10.1007/BF03037169. S2CID 13036056.
• Hanks, S.; McDermott, D. (1987). "Nonmonotonic logic and temporal projection". Artificial Intelligence. 33 (3): 379–412. doi:10.1016/0004-3702(87)90043-9.
• Lin, F.; Zhao, Y. (2004). "ASSAT: Computing answer sets of a logic program by SAT solvers" (PDF). Artificial Intelligence. 157 (1–2): 115–137. doi:10.1016/j.artint.2004.04.004. S2CID 514581.
• Marek, V.; Subrahmanian, V.S. (1989). "The relationship between logic program semantics and non-monotonic reasoning". Logic Programming: Proceedings of the Sixth International Conference. MIT Press. pp. 600–617. ISBN 978-0-262-62065-9.
• Pearce, D. (1997). "A new logical characterization of stable models and answer sets" (PDF). Non-Monotonic Extensions of Logic Programming. Lecture Notes in Artificial Intelligence. Vol. 1216. pp. 57–70. doi:10.1007/BFb0023801. ISBN 978-3-540-68702-3.
• Reiter, R. (1980). "A logic for default reasoning" (PDF). Artificial Intelligence. 13 (1–2): 81–132. doi:10.1016/0004-3702(80)90014-4.