Horn Clauses

From http://foldoc.doc.ic.ac.uk/foldoc/foldoc.cgi?query=horn&action=Search :

A set of atomic literals with at most one positive literal. Usually written

 L <- L1, ..., Ln

or

 <- L1, ..., Ln

where n>=0. If L is false the clause is regarded as a goal. Horn clauses can express a subset of statements of FirstOrderLogic.

The name "Horn Clause" comes from the logician Alfred Horn, who first pointed out the significance of such clauses in 1951, in the article "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

A definite clause is a Horn clause that has exactly one positive literal.

---

I don't know how many people have had the opportunity to program in guarded Horn clauses - it is really quite interesting... especially if the constructs are all order-independent, so they are strictly logical. We created such a language for ourselve in 1988 to describe communication protocols (the point was to add new clauses dynamically, so order independence was quite important to us, and state machines don't fit the bill). -- AlistairCockburn

---

See Also: PrologLanguage