Slide 14.5: Horn clauses

Slide 14.4: Inference rules
Slide 14.6: Examples of Horn clauses
Home

Horn Clauses

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:

     ¬a₁ ∨ ¬a₂ ∨ a₃ ∨ … ∨ ¬a_n ∨ b

It can also be written equivalently in the form of an implication:

     a₁ ∧ a₂ ∧ a₃ ∧ … ∧ a_n → b

The number of a_i'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 ) ).