DLV

The DLV (DataLog with Disjunction, where the logical disjunction symbol V is used) system is a disjunctive logic programming system, implementing the stable model semantics under the answer set programming paradigm. It extends the Datalog language to allow the use of OR in the heads of rules.

Briefly, disjunctive Datalog is a variant of Datalog where disjunctions may appear in the rule heads; advanced versions also allow for negation in the bodies, which can be handled according to a semantics for negation in disjunctive logic programming.

Programming example

The following is a program in Datalog extended with negation as failure:

smoker(john).
smoker(jack).

jogger(jill).
jogger(john).

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

This is the translation of the above program into 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).

The following query has a single stable model:

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

External links

• DLV user manual
• DLV Tutorial