Stabil modellsemantik

Konceptet med en stabil modell , eller svarsuppsättning , används för att definiera en deklarativ semantik för logikprogram med negation som misslyckande . Detta är en av flera standardmetoder för betydelsen av negation i logisk programmering, tillsammans med programslutförande och den välgrundade semantiken . Den stabila modellens semantik är grunden för programmering av svarsuppsättningar .

Motivering

Forskning om den deklarativa semantiken för negation i logisk programmering motiverades av det faktum att beteendet hos SLDNF- upplösning – generaliseringen av SLD-upplösning som används av Prolog i närvaro av negation i regelsamlingarna – inte helt matchar sanningstabellerna som är bekanta från klassisk propositionell logik . Tänk till exempel på programmet

p\

r\leftarrow p,\ q

s\leftarrow p,\ \operatörsnamn {inte} q.

Givet detta program kommer frågan $p$ att lyckas, eftersom programmet inkluderar $p$ som ett faktum; frågan $q$ kommer att misslyckas, eftersom den inte förekommer i huvudet på någon av reglerna. Frågan $r$ kommer också att misslyckas, eftersom den enda regeln med $r$ i huvudet innehåller delmålet $q$ i sin kropp; som vi har sett misslyckas det delmålet. Slutligen, frågan $s$ lyckas, eftersom vart och ett av delmålen $p$ , $\operatorname {not} q$ lyckas. (Det senare lyckas eftersom det motsvarande positiva målet $q$ misslyckas.) Sammanfattningsvis kan beteendet hos SLDNF-upplösning på det givna programmet representeras av följande sanningsuppgift:

$sid$	$q$	$r$	$s$
T	F	F	T .

Å andra sidan kan reglerna för det givna programmet ses som propositionsformler om vi identifierar kommatecken med konjunktion $\land$ , symbolen $\operatorname {not}$ med negation $\neg$ , och samtycker till att behandla $F\leftarrow G$ som implikationen $G\rightarrow F$ skriven baklänges. Till exempel är den sista regeln i det givna programmet, ur denna synvinkel, alternativ notation för propositionsformeln

p\land \neg q\högerpil s.

Om vi beräknar sanningsvärdena för programmets regler för sanningsuppgiften som visas ovan kommer vi att se att varje regel får värdet T . Det uppdraget är med andra ord en modell av programmet. Men detta program har också andra modeller, till exempel

$sid$	$q$	$r$	$s$
T	T	T	F .

Således är en av modellerna för det givna programmet speciell i den meningen att den korrekt representerar beteendet hos SLDNF-upplösning. Vilka är de matematiska egenskaperna hos den modellen som gör den speciell? Ett svar på denna fråga tillhandahålls av definitionen av en stabil modell.

Relation till icke-monotonisk logik

Betydelsen av negation i logikprogram är nära besläktad med två teorier om icke-monotona resonemang - autoepistemisk logik och standardlogik . Upptäckten av dessa samband var ett nyckelsteg mot uppfinningen av den stabila modellens semantik.

Syntaxen för autoepistemisk logik använder en modal operator som tillåter oss att skilja mellan vad som är sant och vad man tror. Michael Gelfond [1987] föreslog att $\operatorname {not} p$ läsa i en regel eftersom " $p$ inte tros", och att förstå en regel med negation som motsvarande formel för autoepistemisk logik. Den stabila modellsemantiken, i sin grundläggande form, kan ses som en omformulering av denna idé som undviker explicita referenser till autoepistemisk logik.

I standardlogik liknar en standard en inferensregel , förutom att den innehåller, förutom sina premisser och slutsatser, en lista med formler som kallas motiveringar. En standard kan användas för att dra sin slutsats under antagandet att dess motiveringar är förenliga med vad man för närvarande tror. Nicole Bidoit och Christine Froidevaux [1987] föreslog att negerade atomer i reglerna skulle behandlas som motiveringar. Till exempel regeln

s\leftarrow p,\ \operatörsnamn {inte} q

kan förstås som standarden som tillåter oss att härleda $s$ från $p$ förutsatt att $\neg q$ är konsekvent. Den stabila modellens semantik använder samma idé, men den hänvisar inte uttryckligen till standardlogik.

Stabila modeller

Definitionen av en stabil modell nedan, återgiven från [Gelfond och Lifschitz, 1988], använder två konventioner. Först identifieras en sanningsuppgift med den mängd atomer som får värdet T . Till exempel sanningsuppdraget

$sid$	$q$	$r$	$s$
T	F	F	T .

identifieras med mängden $\{p,s\}$ . Denna konvention tillåter oss att använda den fastställda inklusionsrelationen för att jämföra sanningsuppdrag med varandra. Den minsta av alla sanningstilldelningar $\emptyset$ är den som gör varje atom falsk; det största sanningsuppdraget gör varje atom sann.

För det andra ses ett logikprogram med variabler som en förkortning för uppsättningen av alla grundinstanser av dess regler, det vill säga resultatet av att variabelfria termer ersätts med variabler i programmets regler på alla möjliga sätt. Till exempel den logiska programmeringsdefinitionen av jämna tal

\operatorname {even} (0)\

\operatorname {even} (s(X))\leftarrow \ operatörsnamn {inte} \operatörsnamn {jämn} (X)

tolkas som resultatet av att $X$ i detta program ersätts med grundvillkoren

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

på alla möjliga sätt. Resultatet är det oändliga markprogrammet

\operatorname {even} (0)\

\operatorname {even} (s(0))\leftarrow \operatorname { not} \operatörsnamn {jämn} (0)

\operatorname {even} (s(s(0)))\leftarrow \operatörsnamn {inte} \operatörsnamn {jämn} (s(0))

\dots

Definition

Låt $P$ vara en uppsättning regler för formen

A\leftarrow B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1}, \dots ,\operatörsnamn {inte} C_{n}

där $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ är malda atomer. Om $P$ inte innehåller negation ( $n=0$ i varje regel i programmet) så är, per definition, den enda stabila modellen av $P$ dess modell som är minimal i förhållande till setinkludering. (Varje program utan negation har exakt en minimal modell.) För att utvidga denna definition till fallet med program med negation behöver vi hjälpkonceptet för reduktion, definierat enligt följande.

För varje uppsättning $I$ av markatomer är reduktionen av $P$ relativt $I$ den uppsättning regler utan negation som erhålls från $P$ genom att först släppa varje regel så att minst en av atomerna $C_{i}$ i dess kropp

B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1},\dots ,\operatörsnamn {not} C_{n}

tillhör $I$ , och sedan släpper delarna $\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}$ från kropparna i alla återstående regler.

Vi säger att $I$ är en stabil modell av $P$ om $I$ är den stabila modellen av reduktionen av $P$ relativt $I$ . (Eftersom reduktionen inte innehåller negation, har dess stabila modell redan definierats.) Som termen "stabil modell" antyder, är varje stabil modell av $P$ en modell av $P$ .

Exempel

För att illustrera dessa definitioner, låt oss kontrollera att $\{p,s\}$ är en stabil modell av programmet

p\

r\leftarrow p,\ q

s\leftarrow p,\ \operatörsnamn {inte} q.

Reduktionen av detta program i förhållande till $\{p,s\}$ är

p\

r\leftarrow p,\ q

s\leftarrow p.

(Faktiskt, eftersom $q\not \in \{p,s\}$ , erhålls reduktionen från programmet genom att släppa delen $\operatorname {not } q.\$ ) Den stabila modellen av redukten är $\{p,s\}$ . (Faktiskt, denna uppsättning atomer uppfyller alla regler för redukten, och den har inga riktiga delmängder med samma egenskap.) Efter $\ {p,s\}}$ ha beräknat den stabila modellen av redukten kom vi alltså fram till samma mängd { p , s som vi började med. Följaktligen är den uppsättningen en stabil modell.

Att på samma sätt kontrollera de andra 15 uppsättningarna som består av atomerna $p,\ q,\ r,\ s$ visar att detta program inte har några andra stabila modeller. Till exempel är reduktionen av programmet i förhållande till $\{p,q,r\}$

p\

r\leftarrow p,\ q.

Den stabila modellen av redukten är $\{p\}$ , vilket skiljer sig från mängden $\{p,q,r\}$ som vi började med .

Program utan en unik stabil modell

Ett program med negation kan ha många stabila modeller eller inga stabila modeller. Till exempel programmet

p\leftarrow \operatörsnamn {inte} q

q\leftarrow \operatörsnamn {inte} p

har två stabila modeller $\{p\}$ , $\{q\}$ . Enregelprogrammet

p\leftarrow \operatörsnamn {inte} p

har inga stabila modeller.

Om vi tänker på den stabila modellens semantik som en beskrivning av beteendet hos Prolog i närvaro av negation så kan program utan en unik stabil modell bedömas som otillfredsställande: de ger inte en entydig specifikation för prolog-liknande frågesvar. Till exempel är de två programmen ovan inte rimliga eftersom Prolog-program – SLDNF-upplösning avslutas inte på dem.

Men användningen av stabila modeller i svarsuppsättningsprogrammering ger ett annat perspektiv på sådana program. I det programmeringsparadigmet representeras ett givet sökproblem av ett logikprogram så att programmets stabila modeller motsvarar lösningar. Då motsvarar program med många stabila modeller problem med många lösningar, och program utan stabila modeller motsvarar olösliga problem. Till exempel pusslet med åtta drottningar 92 lösningar; för att lösa det med svarsuppsättningsprogrammering kodar vi det med ett logikprogram med 92 stabila modeller. Ur denna synvinkel är logikprogram med exakt en stabil modell ganska speciella i svarsuppsättningsprogrammering, som polynom med exakt en rot i algebra.

Egenskaper för den stabila modellens semantik

I det här avsnittet, liksom i definitionen av en stabil modell ovan, menar vi med ett logikprogram en uppsättning regler av formen

A\leftarrow B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1}, \dots ,\operatörsnamn {inte} C_{n}

där $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ är malda atomer.

Huvudatomer: Om en atom $A$ tillhör en stabil modell av ett logiskt program $P$ så är $A$ huvudet för en av reglerna för $P$ .

Minimalitet: Varje stabil modell av ett logikprogram $P$ är minimal bland modellerna av $P$ i förhållande till uppsättningsinkludering.

Antikedjeegenskapen: Om $I$ och $J$ är stabila modeller av samma logikprogram så är $I$ inte en riktig delmängd av $J$ . Med andra ord är uppsättningen av stabila modeller av ett program en antikedja .

NP-fullständighet: Att testa om ett ändligt jordlogikprogram har en stabil modell är NP-komplett .

Relation till andra teorier om negation som misslyckande

Slutförande av programmet

Varje stabil modell av ett ändligt markprogram är inte bara en modell av själva programmet, utan också en modell av dess slutförande [Marek och Subrahmanian, 1989]. Det omvända är dock inte sant. Till exempel slutförandet av enregelprogrammet

p\leftarrow p

är tautologin $p\leftrightarrow p$ . Modellen $\emptyset$ av denna tautologi är en stabil modell av $p\leftarrow p$ , men dess andra modell $\{p\}\$ är det inte. François Fages [1994] fann ett syntaktisk tillstånd på logikprogram som eliminerar sådana motexempel och garanterar stabiliteten för varje modell av programmets slutförande. De program som tillfredsställer hans tillstånd kallas tight .

Fangzhen Lin och Yuting Zhao [2004] visade hur man kan göra slutförandet av ett icke-tight program starkare så att alla dess instabila modeller kommer att elimineras. De ytterligare formlerna som de lägger till i kompletteringen kallas loopformler .

Välgrundad semantik

Den välgrundade modellen av ett logikprogram delar upp alla jordatomer i tre uppsättningar: sant, falskt och okänt. Om en atom är sann i den välgrundade modellen av $P$ så tillhör den varje stabil modell av $P$ . Det omvända håller i allmänhet inte. Till exempel programmet

p\leftarrow \operatörsnamn {inte} q

q\leftarrow \operatörsnamn {not} p

r\leftarrow p

r\leftarrow q

har två stabila modeller, $\{p,r\}$ och $\{q,r\}$ . Även om $r$ tillhör dem båda är dess värde i den välgrundade modellen okänt .

Dessutom, om en atom är falsk i den välgrundade modellen av ett program så tillhör den inte någon av dess stabila modeller. Således ger den välgrundade modellen av ett logikprogram en nedre gräns för skärningspunkten mellan dess stabila modeller och en övre gräns för deras förening.

Stark negation

Representerar ofullständig information

kunskapsrepresentationens perspektiv kan en uppsättning markatomer ses som en beskrivning av ett fullständigt kunskapstillstånd: de atomer som hör till mängden är kända för att vara sanna, och de atomer som inte hör till mängden är känd för att vara falsk. Ett möjligen ofullständigt kunskapstillstånd kan beskrivas med hjälp av en konsekvent men möjligen ofullständig uppsättning bokstavsord; om en atom $p$ inte tillhör mängden och dess negation inte heller tillhör mängden så är det inte känt om $p$ är sant eller falskt.

I samband med logisk programmering leder denna idé till behovet av att skilja mellan två typer av negation — negation som misslyckande , diskuterad ovan, och stark negation , som här betecknas med $\sim$ . Följande exempel, som illustrerar skillnaden mellan de två typerna av negation, tillhör John McCarthy . En skolbuss får korsa järnvägsspår under förutsättning att det inte finns något tåg som närmar sig. Om vi inte nödvändigtvis vet om ett tåg närmar sig så är regeln att använda negation som misslyckande

{\hbox{Cross}}\leftarrow {\hbox{inte tåg}}

är inte en adekvat representation av denna idé: den säger att det är okej att korsa i avsaknad av information om ett annalkande tåg. Den svagare regeln, som använder stark negation i kroppen, är att föredra:

{\hbox{Cross}}\leftarrow \,\sim {\hbox{Tåg}}.

Det står att det är okej att gå över om vi vet att inget tåg närmar sig.

Sammanhängande stabila modeller

För att införliva stark negation i teorin om stabila modeller tillät Gelfond och Lifschitz [1991] vart och ett av uttrycken $A$ , ${\displaystyle B_{i}} ,$ C $\displaystyle C_{i}}$ i en regel

A\leftarrow B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1}, \dots ,\operatörsnamn {inte} C_{n}

att vara antingen en atom eller en atom med den starka negationssymbolen som prefix. Istället för stabila modeller använder denna generalisering svarsuppsättningar , som kan inkludera både atomer och atomer med prefix med stark negation.

Ett alternativt tillvägagångssätt [Ferraris och Lifschitz, 2005] behandlar stark negation som en del av en atom, och det kräver inga förändringar i definitionen av en stabil modell. I denna teori om stark negation skiljer vi mellan atomer av två slag, positiva och negativa , och antar att varje negativ atom är ett uttryck för formen ${\displaystyle \sim A} ,$ där $A\$ är en positiv atom. En uppsättning atomer kallas koherenta om den inte innehåller "komplementära" par av atomer $\ A,\sim A$ . Koherenta stabila modeller av ett program är identiska med dess konsekventa svarsuppsättningar i betydelsen av [Gelfond och Lifschitz, 1991].

Till exempel programmet

p\leftarrow \operatörsnamn {inte} q

q\leftarrow \operatorname {not} p

r\

\sim r\leftarrow \operatörsnamn {inte} p

har två stabila modeller, $\{p,r\}\$ och $\ \{q,r,\sim r\}$ . Den första modellen är sammanhängande; den andra är det inte, eftersom den innehåller både atomen $\ r$ och atomen $\ \sim r$ .

Stängt världsantagande

Enligt [Gelfond och Lifschitz, 1991] kan det slutna världsantagandet för ett predikat $p\$ uttryckas med regeln

\sim p(X_{1},\dots ,X_{n})\vänsterpil \operatörsnamn {inte } p(X_{1},\dots ,X_{n})

(relationen $p\$ gäller inte för en tuppel $X_{1},\dots ,X_{n}$ om det inte finns några bevis för att det gör det). Till exempel den stabila modellen av programmet

p(a,b)\

p(c,d)\

\sim p(X,Y)\leftarrow \operatörsnamn {inte} p(X,Y)

består av 2 positiva atomer

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

och 14 negativa atomer

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

dvs de starka negationerna av alla andra positiva markatomer bildade av $p,\ a,\ b,\ c,\ d$ .

Ett logikprogram med stark negation kan inkludera antagandereglerna för den slutna världen för några av dess predikat och lämna de andra predikaten i det öppna världsantagandets område .

Program med begränsningar

Den stabila modellsemantiken har generaliserats till många typer av logikprogram andra än samlingar av "traditionella" regler som diskuterats ovan - regler i formen

A\leftarrow B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1}, \dots ,\operatörsnamn {inte} C_{n}

där $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ är atomer. En enkel tillägg tillåter program att innehålla begränsningar - regler med det tomma huvudet:

\leftarrow B_{1},\dots ,B_{m},\operatörsnamn {inte} C_{1},\dots ,\operatörsnamn {inte} C_{n}.

Kom ihåg att en traditionell regel kan ses som alternativ notation för en propositionsformel om vi identifierar kommatecken med konjunktion $\land$ , symbolen $\operatorname {not}$ med negation $\neg$ , och samtycker till att behandla $F\leftarrow G$ som implikationen $G\rightarrow F$ skriven baklänges. För att utvidga denna konvention till begränsningar identifierar vi en begränsning med negationen av formeln som motsvarar dess kropp:

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

Vi kan nu utöka definitionen av en stabil modell till program med begränsningar. Som i fallet med traditionella program börjar vi med program som inte innehåller negation. Ett sådant program kan vara inkonsekvent; då säger vi att den inte har några stabila modeller. Om ett sådant program $P$ är konsekvent så har $P$ en unik minimal modell, och den modellen anses vara den enda stabila modellen av $P$ .

Därefter definieras stabila modeller av godtyckliga program med begränsningar med hjälp av redukter, bildade på samma sätt som i fallet med traditionella program (se definitionen av en stabil modell ovan). En uppsättning $I$ av atomer är en stabil modell av ett program $P$ med begränsningar om reduktionen av $P$ relativt $I$ har en stabil modell, och att stabil modell är lika med $I$ .

Egenskaperna för den stabila modellsemantiken som anges ovan för traditionella program gäller även i närvaro av begränsningar.

Restriktioner spelar en viktig roll i svarsuppsättningsprogrammering eftersom att lägga till en begränsning till ett logikprogram $P$ påverkar samlingen av stabila modeller av $P$ på ett mycket enkelt sätt: det eliminerar de stabila modeller som bryter mot begränsning. Med andra ord, för alla program $P$ med begränsningar och alla begränsningar ${\displaystyle C} kan$ de stabila modellerna av $P\cup \{C\}$ karakteriseras som de stabila modellerna av $P$ som uppfyller $C$ .

Disjunktiva program

I en disjunktiv regel kan huvudet vara disjunktionen av flera atomer:

A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m },\operatörsnamn {inte} C_{1},\dots ,\operatörsnamn {inte} C_{n}

(semikolonet ses som alternativ notation för disjunktion ${\displaystyle \lor } )$ . Traditionella regler motsvarar $k=1$ , och begränsningar till $k=0$ . För att utvidga den stabila modellsemantiken till disjunktiva program [Gelfond och Lifschitz, 1991] definierar vi först att i frånvaro av negation ( $n=0$ i varje regel) är de stabila modellerna för ett program dess minimala modeller . Definitionen av reduktionen för disjunktiva program är densamma som tidigare . En mängd $I$ av atomer är en stabil modell av $P$ om $I$ är en stabil modell av reduktionen av $P$ relativt $I$ .

Till exempel är mängden $\{p,r\}$ en stabil modell av det disjunktiva programmet

p;q\

r\leftarrow \operatörsnamn {inte} q

eftersom det är en av två minimala modeller av redukten

p;q\

r.\

Programmet ovan har en mer stabil modell, $\{q\}$ .

Som i fallet med traditionella program är varje element i varje stabil modell av ett disjunktivt program $P$ en huvudatom av ${\displaystyle P} ,$ i den meningen att det förekommer i huvudet av en av reglerna av $P$ . Som i det traditionella fallet är de stabila modellerna av ett disjunktivt program minimala och bildar en antikedja. Att testa om ett ändligt disjunktivt program har en stabil modell är $\Sigma _{2}^{\rm {P}}$ -komplett [Eiter och Gottlob, 1993].

Stabila modeller av en uppsättning propositionsformler

Regler, och även disjunktiva regler , har en ganska speciell syntaktisk form, i jämförelse med godtyckliga propositionsformler . Varje disjunktiv regel är i huvudsak en implikation så att dess antecedent (regelkroppen) är en konjunktion av bokstavliga ord och dess följd (huvud) är en disjunktion av atomer. David Pearce [1997] och Paolo Ferraris [2005] visade hur man utvidgar definitionen av en stabil modell till uppsättningar av godtyckliga propositionsformler. Denna generalisering har applikationer för svarsuppsättningsprogrammering .

Pearces formulering ser väldigt annorlunda ut från den ursprungliga definitionen av en stabil modell . Istället för redukter hänvisar det till jämviktslogik - ett system av icke-monotonisk logik baserat på Kripke-modeller . Ferraris formulering, å andra sidan, är baserad på redukter, även om processen för att konstruera redukten som den använder skiljer sig från den som beskrivs ovan . De två tillvägagångssätten för att definiera stabila modeller för uppsättningar av propositionsformler är likvärdiga med varandra.

Allmän definition av en stabil modell

Enligt [Ferraris, 2005] är reduktionen av en propositionsformel $F$ i förhållande till en uppsättning $I$ av atomer formeln som erhålls från $F$ genom att ersätta varje maximal subformel som är inte nöjd med $I$ med den logiska konstanten $\bot$ (falskt). Reduktionen av en uppsättning $P$ av propositionsformler relativt $I$ består av reduktionerna av alla formler från $P$ relativt $\displaystyle I}$ { . Liksom i fallet med disjunktiva program, säger vi att en mängd $I$ av atomer är en stabil modell av $P$ om $I$ är minimal (med avseende på mängdinkludering) bland modeller av reduktionen av $P$ relativt $I$ .

Till exempel reduktionen av setet

\{p,\ p\land q\högerpil r,\ p\land \neg q\högerpil s\}

relativt till $\{p,s\}$ är

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

Eftersom $\{p,s\}$ är en modell av redukten, och de rätta delmängderna av den mängden inte är modeller av redukten, $\{p, s\}$ är en stabil modell av den givna uppsättningen formler.

Vi har sett att $\{p,s\}$ också är en stabil modell av samma formel, skriven i logisk programmeringsnotation, i betydelsen av den ursprungliga definitionen . Detta är ett exempel på ett allmänt faktum: vid tillämpning på en uppsättning (formler som motsvarar) traditionella regler, är definitionen av en stabil modell enligt Ferraris ekvivalent med den ursprungliga definitionen. Detsamma gäller mer generellt för program med begränsningar och för disjunktiva program .

Egenskaper för den allmänna stabila modellens semantik

Satsen som hävdar att alla element i en stabil modell av ett program $P$ är huvudatomer av $P$ kan utökas till uppsättningar av propositionsformler, om vi definierar huvudatomer enligt följande. En atom $A$ är en huvudatom i en uppsättning $P$ av propositionsformler om minst en förekomst av $A$ i en formel från $P$ varken finns i omfattningen av en negation eller i föregångaren till en implikation. (Vi antar här att ekvivalens behandlas som en förkortning, inte ett primitivt bindemedel.)

Minimaliteten och antikedjeegenskapen hos stabila modeller av ett traditionellt program håller inte i det allmänna fallet. Till exempel (den singleton-uppsättning som består av) formeln

p\lor \neg p

har två stabila modeller, $\emptyset$ och $\{p\}$ . Det senare är inte minimalt, och det är en riktig superset av det förra.

Att testa om en ändlig uppsättning satsformler har en stabil modell är $\Sigma _{2}^{\rm {P}}$ -komplett , som i fallet med disjunktiva program .

Se även

Anteckningar

Bidoit, N.; Froidevaux, C. (1987). "Minimalism subsumerar standardlogik och omskrivning". Proceedings: Symposium on Logic in Computer Science, Ithaca, New York, 22-25 juni 1987 . IEEE Computer Society Press. s. 89–97. ISBN 978-0-8186-0793-6 . 87CH2464-6.
Eiter, T.; Gottlob, G. (1993). "Komplexitetsresultat för disjunktiv logikprogrammering och tillämpning på icke-monotona logik" . ILPS '93: Proceedings of the 1993 international symposium on logic programmering . MIT Press. s. 266–278. ISBN 978-0-262-63152-5 .
van Emden, M.; Kowalski, R. (1976). "Predikatlogikens semantik som programmeringsspråk" (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). "Konsekvens av Clarks färdigställande och existens av stabila modeller" . Journal of Methods of Logic in Computer Science . 1 : 51–60. CiteSeerX 10.1.1.48.2157 .
Ferraris, P. (2005). "Svarsuppsättningar för propositionella teorier" . Logisk programmering och icke-monotona resonemang. LPNMR 2005 . Föreläsningsanteckningar i datavetenskap. Vol. 3662. Springer. s. 119–131. CiteSeerX 10.1.1.129.5332 . doi : 10.1007/11546207_10 . ISBN 978-3-540-31827-9 .
Ferraris, P.; Lifschitz, V. (2005). "Matematiska grunder för programmering av svarsuppsättningar" . Vi kommer att visa dem! Uppsatser till ära av Dov Gabbay . King's College Publications. s. 615–664. CiteSeerX 10.1.1.79.7622 .
Gelfond, M. (1987). "Om stratifierade autoepistemiska teorier" (PDF) . AAAI'87: Proceedings of the sjätte nationella konferensen om artificiell intelligens . s. 207–211. ISBN 978-0-934613-42-2 .
Gelfond, M.; Lifschitz, V. (1988). "Den stabila modellens semantik för logisk programmering" . Proceedings of the Fifth International Conference on Logic Programming (ICLP) . MIT Press. s. 1070–80. ISBN 978-0-262-61054-4 .
Gelfond, M.; Lifschitz, V. (1991). "Klassisk negation i logikprogram och disjunktiva databaser" . Ny generation datoranvändning . 9 (3–4): 365–385. CiteSeerX 10.1.1.49.9332 . doi : 10.1007/BF03037169 . S2CID 13036056 .
Hanks, S.; McDermott, D. (1987). "Ickemonotonisk logik och tidsprojektion" . Artificiell intelligens . 33 (3): 379–412. doi : 10.1016/0004-3702(87)90043-9 .
Lin, F.; Zhao, Y. (2004). "ASSAT: Beräknar svarsuppsättningar av ett logikprogram av SAT-lösare" (PDF) . Artificiell intelligens . 157 (1–2): 115–137. doi : 10.1016/j.artint.2004.04.004 . S2CID 514581 .
Marek, V.; Subrahmanian, VS (1989). "Förhållandet mellan logikprogram semantik och icke-monotona resonemang". Logisk programmering: Proceedings of the Sixth International Conference . MIT Press. s. 600–617. ISBN 978-0-262-62065-9 .
Pearce, D. (1997). "En ny logisk karakterisering av stabila modeller och svarsuppsättningar" (PDF) . Icke-monotona utökningar av logisk programmering . Föreläsningsanteckningar i artificiell intelligens. Vol. 1216. s. 57–70. doi : 10.1007/BFb0023801 . ISBN 978-3-540-68702-3 .
Reiter, R. (1980). "En logik för standardresonemang" (PDF) . Artificiell intelligens . 13 (1–2): 81–132. doi : 10.1016/0004-3702(80)90014-4 .