DLV
DLV- systemet ( D ata L og med Disjunction, där den logiska disjunktionssymbolen V används) är ett disjunktivt logiskt programmeringssystem , som implementerar den stabila modellsemantiken under Answer set-programmeringsparadigmet . Det utökar dataloggspråket för att tillåta användning av OR i regler.
Kortfattat är disjunktiv Datalog en variant av Datalog där disjunktioner kan förekomma i regelhuvudena; avancerade versioner tillåter även negation i kropparna, vilket kan hanteras enligt en semantik för negation i disjunktiv logikprogrammering.
En disjunktiv Datalog-regel är en klausul i formen:
En disjunktiv Datalog-begränsning är en klausul av formen:
En av de mest populära icke-monotona logikerna är Reiters [1980] standardlogik. Denna logik utvecklades som en kunskapsrepresentationsformalism och var ursprungligen inte tänkt som ett databasfrågespråk. Däremot definierades en lämplig inställning där standardlogik kan användas som frågespråk för relationsdatabaser (Default Query Language, DQL).
Ur en praktisk synvinkel, i sammanhanget med deduktiva databaser, verkar disjunktiv Datalog vara den lämpligare förlängningen av DATALOG~ än DQL. På grund av sin enkla syntax, DATALOGv,~ är den mottaglig för automatisk programanalys och optimering.
Dessa resultat är inte bara av teoretiskt intresse; problem som är relevanta i praktiken som att beräkna det optimala resevärdet i Traveling Salesman Problem- och egenvektorberäkningar kan hanteras i disjunktiv Datalog, men inte Datalog med negation (såvida inte polynomhierarkin kollapsar ).
Exempelinmatning: Datalogg med negation som fel
rökare ( john ). rökare ( jack ). joggare ( jill ). joggare ( john ). frisk ( X ) :- joggare ( X ), \+ rökare ( X ).
Översättning till DLV: Ta Clark Completion and Clausal Form
rökare(X) <- X=john. rökare(X) <- X=jack. X=john v X=jack <- smoker(X). jogger(X) <- X=jill. jogger(X) <- X=john. X=jill v X=john <- jogger(X). frisk(X) v rökare(X) <- jogger(X). jogger(X) <- frisk(X) <- frisk(X) & rökare(X).
Exempelkörning: Enkel stabil modell
?- frisk(X). X = jill; Nej
externa länkar