Horn clause

From Exampleproblems

In logic, and in particular in propositional calculus, a Horn clause or a definite clause is a proposition of the general type

(p and q and ... and t) implies u,

where the number of propositions combined by ands is as large as we like (and may be zero).

This form can be rewritten, assuming we are working within the usual classical logic. The usual expression of the logical conditional as a disjunction is the case of the equivalence of

p implies u,

with

(not p) or u.

This generalizes to the equivalence of the general Horn clause expression above with

(not p) or ... or (not t) or u.

In other words, a Horn clause is a simple disjunction in which at most one of the terms is a positive literal, and the rest are negated. This also shows that the conjunction of a set of Horn clauses is in conjunctive normal form. Horn clauses play a basic role in logic programming and are important for constructive logic.

The relevance of Horn clauses to theorem proving by first-order resolution is that the resolution of two Horn clauses is a Horn clause. In automated theorem proving, this can lead to greater efficiencies in representation of the clauses on a computer. In fact, Prolog is a programming language constructed entirely out of Horn clauses.

Horn clauses are also critical in computational complexity, where the problem of finding a set of variable assignments to make a conjunction of Horn clauses true is a P-complete problem, sometimes called HORNSAT. This is P's version of the boolean satisfiability problem, a central NP-complete problem.

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.

Template:FOLDOCcs:Hornova klauzule de:Horn-Formel es:Cláusula de Horn fr:Clause de Horn hu:Horn-klóz pl:Klauzula Horna zh:Horn子句