DLV - DLV

Den DLV ( D ata l og med motsetninger, hvor den logiske motsetninger symbolet V blir brukt) system er en disjunktiv logikk programmeringssystemet, å gjennomføre de stabil modell semantikk under svar sett programmerings paradigme. Det utvider datalog -språket for å tillate bruk av OR i regler.

Kort sagt, disjunctive Datalog er en variant av Datalog der disjunksjoner kan vises i regelhodene; avanserte versjoner tillater også negasjon i kroppene, som kan håndteres i henhold til en semantikk for negasjon i disjunktiv logisk programmering.

En disjunktiv Datalog -regel er en klausul i skjemaet:

En disjunktiv Datalog -begrensning er en klausul i skjemaet:

En av de mest populære ikke -monotone logikkene er Reiters [1980] standardlogikk. Denne logikken ble utviklet som en kunnskapsrepresentasjonsformalisme og ble opprinnelig ikke oppfattet som et databasesøksspråk. Imidlertid ble det definert en passende innstilling der standardlogikk kan brukes som et spørrespråk for relasjonsdatabaser (Standard Query Language, DQL).

Fra et praktisk synspunkt synes disjunktiv Datalog i sammenheng med deduktive databaser å være den mer passende forlengelsen av DATALOG ~ enn DQL. På grunn av sin enkle syntaks, er DATALOGv, ~ tilgjengelig for automatisk programanalyse og optimalisering.

Disse resultatene er ikke bare av teoretisk interesse; problemer som er relevante i praksis, for eksempel å beregne den optimale turverdien i Traveling Salesman Problem og egenvektorberegninger kan håndteres i disjunktiv Datalog, men ikke Datalog med negasjon (med mindre det polynomiske hierarkiet kollapser).

Eksempel på input: Datalog med negasjon som feil

smoker(john).
smoker(jack).

jogger(jill).
jogger(john).

healthy(X) :- jogger(X), \+ smoker(X).

Oversettelse til DLV: Take Clark Completion and Clausal Form

smoker(X) <- X=john.
smoker(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).

healthy(X) v smoker(X) <- jogger(X).
jogger(X) <- healthy(X)
<- healthy(X) & smoker(X).

Eksempelkjøring: Enkeltstabil modell

?- healthy(X).
X = jill ;
No

Referanser

Eksterne linker