Horn clauses can be used to express most, but not all, logical statements.
A Horn clause is defined as follows:
A Horn clause is a clause (a disjunction of literals) with at most one positive literal.
where
- a literal is an atom or its negation,
- disjunction is the operation “or,” and
- a positive literal is just an atom.
The following is an example of a (definite) Horn clause:
¬a1 ∨ ¬a2 ∨ a3 ∨ … ∨ ¬an ∨ b
It can also be written equivalently in the form of an implication:
a1 ∧ a2 ∧ a3 ∧ … ∧ an → b
The number of ai's may be 0, in which case the Horn clause has the form
→ b
Such a clause means that b is always true, that is, b is an axiom and is usually written without the connective →.
The following statements from previous example are written in first-order predicate calculus:
natural( 0 ).
for all x, natural( x ) → natural( successor( x ) ).
These can be translated into Horn clauses by dropping the quantifier:
natural( 0 ).
natural( x ) → natural( successor( x ) ).