Horn clauses

A Horn clause is a logical formula of the form

   a_1 \land \dots \land a_n \to b

where the a_i's and b are literals.

Horn clauses are traditionally written the other way around, i.e.

  b \leftarrow a_1 \land \dots \land a_n

Horn clauses are of central importance in logic programming.

Specific forms

Facts

If i = 0, i.e. there are no a_i's, then the clause is of the form

b \leftarrow \top

(where \top is truth).

This is referred to as a fact or ground truth, as it forces b to be true.

Goals

If b = \bot (where \bot is falsity), then the clause is of the form

\bot \leftarrow a_1 \land \dots \land a_n

This is referred to as a goal. This is because Horn clauses are usually used with proof systems that are refutation complete, such as resolution. Such systems are able to prove \bot from a set of contradictory clauses, if such a thing is possible.

We can add a goal clause to a set of clauses, and then try to find a proof of \bot. Then, if we find one, we must have proved all the a_i's in the process.

References

• Wikipedia page

• Horn clauses were introduced by Alfred Horn in a 1951 JSL paper:

@article{horn_1951,
	title = {On sentences which are true of direct unions of algebras},
  volume = {16},
  doi = {10.2307/2268661},
  number = {1},
  journal = {Journal of Symbolic Logic},
  publisher = {Cambridge University Press},
  author = {Horn, Alfred},
  year = {1951},
  pages = {14–21}
}