Editing Horn clause

{{Short description|Type of logical formula}}
In [[mathematical logic]] and [[logic programming]], a '''Horn clause''' is a [[logical formula]] of a particular rule-like form that gives it useful properties for use in logic programming, [[formal specification]], [[universal algebra]] and [[model theory]]. Horn clauses are named for the logician [[Alfred Horn]], who first pointed out their significance in 1951.{{sfn|Horn|1951}}

== 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}}

==Logic programming==

Horn clauses are also the basis of [[logic programming]], where it is common to write definite clauses in the form of an [[Material conditional|implication]]:

{{block indent|(''p'' ∧ ''q'' ∧ ... ∧ ''t'') → ''u''}}

In fact, the resolution of a goal clause with a definite clause to produce a new goal clause is the basis of the [[SLD resolution]] inference rule, used in implementation of the logic programming language [[Prolog]].

In logic programming, a definite clause behaves as a goal-reduction procedure. For example, the Horn clause written above behaves as the procedure:

{{block indent|to show ''u'', show ''p'' and show ''q'' and ... and show ''t''.}}

To emphasize this reverse use of the clause, it is often written in the reverse form:

{{block indent|''u'' ← (''p'' ∧ ''q'' ∧ ... ∧ ''t'')}}

In [[Prolog]] this is written as:

<syntaxhighlight lang="prolog">u :- p, q, ..., t.</syntaxhighlight>

In logic programming, a goal clause, which has the logical form

{{block indent|∀''X'' (''false'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'')}}

represents the negation of a problem to be solved. The problem itself is an existentially quantified conjunction of positive literals:

{{block indent|∃''X'' (''p'' ∧ ''q'' ∧ ... ∧ ''t'')}}

The Prolog notation does not have explicit quantifiers and is written in the form:

<syntaxhighlight lang="prolog">:- p, q, ..., t.</syntaxhighlight>

This notation is ambiguous in the sense that it can be read either as a statement of the problem or as a statement of the denial of the problem. However, both readings are correct. In both cases, solving the problem amounts to deriving the empty clause. In Prolog notation this is equivalent to deriving:
<syntaxhighlight lang="prolog">:- true.</syntaxhighlight>

If the top-level goal clause is read as the denial of the problem, then the empty clause represents ''false'' and the proof of the empty clause is a refutation of the denial of the problem. If the top-level goal clause is read as the problem itself, then the empty clause represents ''true'', and the proof of the empty clause is a proof that the problem has a solution. 

The solution of the problem is a substitution of terms for the variables ''X'' in the top-level goal clause, which can be extracted from the resolution proof.  Used in this way, goal clauses are similar to [[conjunctive query|conjunctive queries]] in [[relational database]]s, and Horn clause logic is equivalent in computational power to a [[universal Turing machine]]. 

Van Emden and Kowalski (1976) investigated the model-theoretic properties of Horn clauses in the context of logic programming, showing that every set of definite clauses '''D''' has a unique minimal model '''M'''. An [[atomic formula]] '''A''' is logically implied by '''D''' if and only if '''A''' is true in '''M'''. It follows that a problem '''P''' represented by an existentially quantified conjunction of positive literals is logically implied by '''D''' if and only if '''P''' is true in '''M'''. The minimal model semantics of Horn clauses is the basis for the [[stable model semantics]] of logic programs.{{sfn|van Emden|Kowalski|1976}}

== See also ==
*[[Constrained Horn clauses]]
*[[Propositional calculus]]

== Notes==
{{reflist}}

== References ==
*{{cite book
|editor-last1= Burris
|editor-first1=Stanley
|editor-last2=Sankappanavar
|editor-first2=H.P.
|year=1981
|url=https://archive.org/details/courseinuniversa00stan
|title=A Course in Universal Algebra
|publisher=Springer-Verlag
|isbn=0-387-90578-2
|url-access=registration
}}
*{{cite book
| last=Buss
| first=Samuel R.
| authorlink = Samuel Buss
| year=1998
| isbn=978-0-444-89840-1
| issn=0049-237X
| editor = Samuel R. Buss
| title=Handbook of Proof Theory
| publisher=Elsevier B.V
| series=Studies in Logic and the Foundations of Mathematics
| volume=137
| contribution=An Introduction to Proof Theory
| pages=1&ndash;78
| contribution-url=http://www.sciencedirect.com/science/article/pii/S0049237X98800165
| doi=10.1016/S0049-237X(98)80016-5
}}
*{{Cite book
| last1=Chang
| first1=Chen Chung
| author-link=Chen Chung Chang
| last2=Keisler
| first2=H. Jerome
| author2-link=Howard Jerome Keisler
| title=Model Theory
| orig-year=1973
| publisher=Elsevier
| edition=3rd
| series=Studies in Logic and the Foundations of Mathematics
| isbn=978-0-444-88054-3
| year=1990
}}
*{{cite journal
|last1=Dowling
|first1=William F.
|last2=Gallier
|first2=Jean H.
|author2-link= Jean Gallier
|year=1984
|title=Linear-time algorithms for testing the satisfiability of propositional Horn formulae
|journal=[[Journal of Logic Programming]]
|volume=1
|number=3
|pages=267–284
|doi=10.1016/0743-1066(84)90014-1|doi-access=free
}}
*{{cite journal
|last1=van Emden
|first1=M. H.
|author-link1=Maarten van Emden
|last2=Kowalski
|first2=R. A.
|author-link2=Robert Kowalski
|year=1976
|url=http://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf
|title=The semantics of predicate logic as a programming language
|journal=[[Journal of the ACM]]
|volume=23
|number=4
|pages=733–742
|doi=10.1145/321978.321991|citeseerx=10.1.1.64.9246
|s2cid=11048276
}}
*{{cite journal
|last=Horn
|first=Alfred
|author-link=Alfred Horn
|year=1951
|title=On sentences which are true of direct unions of algebras
|journal=[[Journal of Symbolic Logic]]
|pages=14–21
|volume=16
|number=1
|doi=10.2307/2268661|jstor=2268661
|s2cid=42534337
}}
*{{cite book
|last1=Lau
|first1=Kung-Kiu
|last2=Ornaghi
|first2=Mario
|year=2004
|title=Program Development in Computational Logic
|chapter=Specifying Compositional Units for Correct Program Development in Computational Logic
|series=Lecture Notes in Computer Science
|volume=3049
|pages=1–29
|doi=10.1007/978-3-540-25951-0_1
|isbn=978-3-540-22152-4
}}
*{{cite journal
|last=Makowsky
|first=J.A.
|author-link=Johann Makowsky
|year=1987
|url=https://core.ac.uk/download/pdf/82190596.pdf
|title=Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples
|journal=[[Journal of Computer and System Sciences]]
|volume=34
|issue=2–3
|pages=266&ndash;292
|doi=10.1016/0022-0000(87)90027-4
|doi-access=free
}}

{{DEFAULTSORT:Horn clause}}
[[Category:Logic in computer science]]
[[Category:Normal forms (logic)]]
{{Normal forms in logic}}