In logic, and in particular in propositional calculus, a Horn 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 generalises to the equivalence of the general Horn clause expression above with

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

This form shows that Horn clauses are a subset of those in conjunctive normal form, in which at most one of the terms is a positive literal, and the rest are negated. 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.