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

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

प्रेरणा

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

$p\$

$r\leftarrow p,\ q$

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

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

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.

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

नॉनमोनोटोनिक लॉजिक से संबंध

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

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

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

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

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

स्थिर मॉडल

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

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$

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

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

लेकिन उत्तर सेट प्रोग्रामिंग में स्थिर मॉडलों का उपयोग ऐसे कार्यक्रमों पर अलग दृष्टिकोण प्रदान करता है। उस प्रोग्रामिंग प्रतिमान में, दी गई खोज समस्या तर्क कार्यक्रम द्वारा प्रस्तुत की जाती है ताकि कार्यक्रम के स्थिर मॉडल समाधान के अनुरूप हों। तब कई स्थिर मॉडल वाले प्रोग्राम कई समाधानों के साथ समस्याओं के अनुरूप होते हैं, और बिना स्थिर मॉडल वाले प्रोग्राम अघुलनशील समस्याओं के अनुरूप होते हैं। उदाहरण के लिए, आठ रानियों की पहेली के 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.