Editing Horn clause (section)

== Definition ==

A Horn clause is a disjunctive [[clause (logic)|clause]] (a [[disjunction]] of [[literal (mathematical logic)|literals]]) with at most one positive, i.e. [[negation|unnegated]], literal. 

Conversely, a disjunction of literals with at most one negated literal is called a '''dual-Horn clause'''. 

A Horn clause with exactly one positive literal is a '''definite clause''' or a '''strict Horn clause''';{{sfn|Makowsky|1987}} a definite clause with no negative literals is a '''unit clause''',{{sfn|Buss|1998}} and a unit clause without variables is a '''fact''';{{sfn|Lau|Ornaghi|2004}}
a Horn clause without a positive literal is a '''goal clause'''.
The empty clause, consisting of no literals (which is equivalent to ''false''), is a goal clause.
These three kinds of Horn clauses are illustrated in the following [[Propositional formula|propositional]] example:
{|class="wikitable"
|-
!Type of Horn clause
!Disjunction form
![[Material conditional|Implication]] form
!Read intuitively as
|- align="center"
|'''Definite clause'''
|¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t'' ∨ ''u''
|| ''u'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' 
|| assume that,<BR>if ''p'' and ''q'' and ... and ''t'' all hold, then also ''u'' holds
|-align="center"
|'''Fact'''
|''u'' 
||''u'' ← ''true''               
||assume that<BR>''u'' holds
|-align="center"
|'''Goal clause'''
| ¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t''
|| ''false'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' 
|| show   that<BR>''p'' and ''q'' and ... and ''t'' all hold<ref>Like in [[Resolution_(logic)#A_resolution_technique|resolution theorem proving]], "show φ" and "assume ¬φ" are synonymous ([[indirect proof]]); they both correspond to the same formula, viz. ¬φ.</ref>
|}

All variables in a clause are implicitly [[Universal quantification|universally quantified]] with the scope being the entire clause. Thus, for example:

{{block indent|¬ ''human''(''X'') ∨ ''mortal''(''X'')}}

stands for:

{{block indent|∀X( ¬ ''human''(''X'') ∨ ''mortal''(''X'') ),}}

which is logically equivalent to:

{{block indent|∀X ( ''human''(''X'') → ''mortal''(''X'') ).}}

===Significance===
Horn clauses play a basic role in [[constructive logic]] and [[computational logic]]. They are important in [[automated theorem proving]] by [[first-order resolution]], because the [[Resolution (logic)|resolvent]] of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiency of proving a theorem: the goal clause is the negation of this theorem; see ''Goal clause'' in the above table. Intuitively, if we wish to prove φ, we assume ¬φ (the goal) and check whether such assumption leads to a contradiction. If so, then φ must hold. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).

Propositional Horn clauses are also of interest in [[Computational complexity theory|computational complexity]]. The problem of finding truth-value assignments to make a conjunction of propositional Horn clauses true is known as [[Horn-satisfiability|HORNSAT]]. This problem is [[P-complete]] and solvable in [[linear time]].{{sfn|Dowling|Gallier|1984}} In contrast, the unrestricted [[Boolean satisfiability problem]] is an [[NP-complete]] problem.

In [[universal algebra]], definite Horn clauses are generally called [[Quasi-identity|quasi-identities]]; classes of algebras definable by a set of quasi-identities  are called [[Quasivariety|quasivarieties]] and enjoy some of the good properties of the more restrictive notion of a [[variety (universal algebra)|variety]], i.e., an equational class.{{sfn|Burris|Sankappanavar|1981}} From the model-theoretical point of view, Horn sentences are important since they are exactly (up to logical equivalence) those sentences preserved under [[reduced product]]s; in particular, they are preserved under [[direct product]]s. On the other hand, there are sentences that are not Horn but are nevertheless preserved under arbitrary direct products.{{sfn|Chang|Keisler|1990|loc=Section 6.2}}