Horn Clauses

A definite Horn clause is a clause with at most one positive literal: \(\neg x_1\lor\neg x_2\lor\cdots\lor\neg x_n\)

Normally written as \(x_n\gets(x_1\land x_2\cdots)\)

A fact \(u\) is \(u\gets\vert\)

In a goal Horn clause, all literals are negative, written as \(\bot\gets(x_1\land x_2\land\cdots\land x_n)\)

Propositional HORNSAT is the problem of finding a truth assignment for a conjunction of Horn clauses: P-complete

Prolog

Generalization to FOL, using predicates in Horn clauses.

Prolog is Turing-complete, therefore undecidable.

The resolution method is called SLD (may not terminate in general cases)

A subset of Prolog with a different evaluation mechanism that is decidable.

Compared to Prolog, Datalog:

disallows complex terms as arguments of predicates
requires that every variable that appears in the head of a clause also appear in a positive (not negated) atom in the body of the clause
requires that every variable appearing in a negative literal in the body of a clause also appear in some positive literal in the body of the clause

A logic programming language inspired by Datalog.

Used for program analysis.

Cclyzer++ for C/C++

Doop for Java