form:

:A if B₁ and ... and B_n.

In the simplest case of Horn clauses (or "definite" clauses), which are a subset of first-order logic, all of the A, B₁, ..., B_n are atomic formulae.

Although Horn clause logic programs are Turing complete, for many practical applications, it is useful to extend Horn