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

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

प्रेरणा

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

$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 इसका मॉडल है जो समूह समावेशन के सापेक्ष न्यूनतम है। (निषेध के बिना किसी भी प्रोग्राम में बिल्कुल न्यूनतम मॉडल होता है।) इस परिभाषा को नकारात्मकता वाले कार्यक्रमों के मामले में विस्तारित करने के लिए, हमें निम्न रूप से परिभाषित रिडक्ट की सहायक अवधारणा की आवश्यकता है।

किसी भी समूह के लिए {{mvar|I}जमीन के परमाणुओं की, की कमी P के सापेक्ष I नियमों का वह समुच्चय है, जिससे निषेधन प्राप्त नहीं होता है 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 की कमी का स्थिर मॉडल है P के सापेक्ष I. (चूंकि रिडक्ट में नकारात्मकता सम्मलित नहीं है, इसका स्थिर मॉडल पहले ही परिभाषित किया जा चुका है।) जैसा कि शब्द स्थिर मॉडल से पता चलता है, प्रत्येक स्थिर मॉडल 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 स्थिर मॉडल वाले तर्क प्रोग्राम द्वारा एन्कोड करते हैं। इस दृष्टिकोण से, ठीक स्थिर मॉडल वाले तर्क प्रोग्राम उत्तर समूह प्रोग्रामिंग में विशेष होते हैं, जैसे बीजगणित में ठीक जड़ वाले बहुपद।

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

इस खंड में, जैसा कि ऊपर #Definition में है, तर्क प्रोग्राम से हमारा तात्पर्य फॉर्म के नियमों के समूह से है

$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. दूसरे शब्दों में, प्रोग्राम के स्थिर मॉडल का समूह antichain है।

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

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

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

परिमित जमीनी प्रोग्राम का कोई भी स्थिर मॉडल न केवल प्रोग्राम का मॉडल है, बल्कि विफलता के रूप में इसकी नकारात्मकता का मॉडल भी है # पूर्णता शब्दार्थ [मारेक और सुब्रह्मण्यन, 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$ बाधाओं के साथ अगर की कमी $P$ के सापेक्ष $I$ स्थिर मॉडल है, और वह स्थिर मॉडल बराबर है $I$.

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

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

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

Main article: Disjunctive Datalog

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

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

(अर्धविराम को संयोजन के लिए वैकल्पिक अंकन के रूप में देखा जाता है $\lor$). पारंपरिक नियम इसके अनुरूप हैं $k=1$, और #Programs के लिए बाधाओं के साथ $k=0$. डिसजंक्टिव प्रोग्राम्स [Gelfond and Lifschitz, 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}}$-पूरा [Eiter और गोटलॉब, 1993]।

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

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

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

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

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

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

$\{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\}$ # परिभाषा के अर्थ में तर्क प्रोग्रामिंग नोटेशन में लिखे गए उसी सूत्र का स्थिर मॉडल भी है। यह सामान्य तथ्य का उदाहरण है: पारंपरिक नियमों के समूह (सूत्रों के अनुरूप) के आवेदन में, फेरारीस के अनुसार स्थिर मॉडल की परिभाषा मूल परिभाषा के बराबर है। वही सच है, अधिक आम तौर पर, #Programs with Constraints और #Disjunctive Programs के लिए।

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

प्रमेय यह दावा करता है कि किसी प्रोग्राम के किसी भी स्थिर मॉडल के सभी तत्व $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.