Editing Horn clause (section)

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