Disjunctive Datalog

A disjunctive Datalog program is a collection of rules. A rule is a clause of the form:[2]

${\displaystyle a_{1}\vee \dots \vee a_{n}\leftarrow b_{1}\wedge \dots \wedge b_{m}\quad 1\leq n,0\leq m}$

where ${\displaystyle b_{1}}$, ..., ${\displaystyle b_{m}}$ may be negated, and may include (in)equality constraints.

There are at least three ways to define the semantics of disjunctive Datalog:[3]

• Minimal model semantics
• Perfect model semantics
• Disjunctive stable model semantics, which generalizes the stable model semantics

Disjunctive Datalog can express several NP-complete and NP-hard problems, including the travelling salesman problem, graph coloring, maximum clique problem, and minimal vertex cover.[3] These problems are only expressible in Datalog if the polynomial hierarchy collapses.

The DLV (DataLog with Disjunction, where the logical disjunction symbol V is used) system implements the disjunctive stable model semantics.[4]

• Syntax and semantics of logic programming