Horn Clause

A horn clause is a clause containing at most one positive literal.

Horn clauses with exactly one positive literal (definite clauses) can be written in an implication form without making use of the negation symbol: L_pos ← L₁ ∧ L₂ ∧ ... ∧ L_n.

The positive Literal L_pos is called the conclusion or the head of the horn clause. The literals L_i, i ∈ {1, ..., n} are the negations of the negative literals (same literals without the negation symbol), which form the preconditions, or, all together, the body of the clause.