Editing Logic programming (section)

=== Semantics of Horn clause programs ===

{{main|Syntax and semantics of logic programming}}

Viewed in purely logical terms, there are two approaches to the declarative semantics of Horn clause logic programs: One approach is the original ''[[logical consequence]] semantics'', which understands solving a goal as showing that the goal is a theorem that is true in all [[Structure (mathematical logic)#Structures and first-order logic|models]] of the program.

In this approach, computation is [[Automated theorem proving|theorem-proving]] in [[first-order logic]]; and both [[backward chaining|backward reasoning]], as in SLD resolution, and [[forward chaining|forward reasoning]], as in hyper-resolution,  are correct and complete theorem-proving methods.  Sometimes such theorem-proving methods are also regarded as providing a separate [[proof-theoretic semantics|proof-theoretic (or operational) semantics]] for logic programs. But from a logical point of view, they are proof methods, rather than semantics.

The other approach to the declarative semantics of Horn clause programs is the ''[[satisfiability]] semantics'', which understands solving a goal as showing that the goal is true (or satisfied) in some [[intended interpretation|intended (or standard) model]] of the program. For Horn clause programs, there always exists such a standard model: It is the unique ''minimal model'' of the program.

Informally speaking, a minimal model is a model that, when it is viewed as the set of all (variable-free) facts that are true in the model, contains no smaller set of facts that is also a model of the program.

For example, the following facts represent the minimal model of the family relationships example in the introduction of this article. All other variable-free facts are false in the model:

<syntaxhighlight lang="prolog">
mother_child(elizabeth, charles).
father_child(charles, william).
father_child(charles, harry).
parent_child(elizabeth, charles).
parent_child(charles, william).
parent_child(charles, harry).
grandparent_child(elizabeth, william).
grandparent_child(elizabeth, harry).
</syntaxhighlight>

The satisfiability semantics also has an alternative, more mathematical characterisation as the [[least fixed point]] of the function that uses the rules in the program to derive new facts from existing facts in one step of inference.

Remarkably, the same problem-solving methods of forward and backward reasoning, which were originally developed for the logical consequence semantics, are equally applicable to the satisfiability semantics: Forward reasoning generates the minimal model of a Horn clause program, by deriving new facts from existing facts, until no new additional facts can be generated. Backward reasoning, which succeeds by reducing a goal to subgoals, until all subgoals are solved by facts, ensures that the goal is true in the minimal model, without generating the model explicitly.<ref>{{cite journal|last1=Van Emden|first1=M.H.|last2=Kowalski|first2=R.A.|date=October 1976|title=The semantics of predicate logic as a programming language|journal=[[Journal of the ACM]]|volume=23|issue=4|pages=733–742|doi=10.1145/321978.321991 |s2cid=11048276 |doi-access=free}}</ref>

The difference between the two declarative semantics can be seen with the definitions of addition and multiplication in [[Peano arithmetic#Defining arithmetic operations and relations|successor arithmetic]], which represents the natural numbers <code>0, 1, 2, ...</code> as a sequence of terms of the form <code>0, s(0), s(s(0)), ...</code>. In general, the term <code>s(X)</code> represents the successor of <code>X,</code> namely <code>X + 1.</code> Here are the standard definitions of addition and multiplication in functional notation:
<pre>
     X + 0 = X.
     X + s(Y)    = s(X + Y). 
i.e. X + (Y + 1) = (X + Y) + 1

     X × 0 = 0.
     X × s(Y)    = X + (X × Y). 
i.e. X × (Y + 1) = X + (X × Y).
</pre>
Here are the same definitions as a logic program, using <code>add(X, Y, Z)</code> to represent <code>X + Y = Z,</code> and <code>multiply(X, Y, Z)</code> to represent <code>X × Y = Z</code>:
<syntaxhighlight lang="prolog">
add(X, 0, X).
add(X, s(Y), s(Z)) :- add(X, Y, Z).

multiply(X, 0, 0).
multiply(X, s(Y), W) :- multiply(X, Y, Z), add(X, Z, W).
</syntaxhighlight>

The two declarative semantics both give the same answers for the same existentially quantified conjunctions of addition and multiplication goals. For example <code>2 × 2 = X</code> has the solution <code>X = 4</code>; and <code>X × X = X + X</code> has two solutions <code>X = 0</code> and <code>X = 2</code>:

<syntaxhighlight lang="prolog">
?- multiply(s(s(0)), s(s(0)), X).
X = s(s(s(s(0)))).

?- multiply(X, X, Y), add(X, X, Y).
X = 0, Y = 0.
X = s(s(0)), Y = s(s(s(s(0)))).
</syntaxhighlight>

However, with the logical-consequence semantics, there are non-standard models of the program, in which, for example, <code>add(s(s(0)), s(s(0)), s(s(s(s(s(0)))))),</code> i.e. <code>2 + 2 = 5</code> is true. But with the satisfiability semantics, there is only one model, namely the standard model of arithmetic, in which <code>2 + 2 = 5</code> is false.

In both semantics, the goal <syntaxhighlight lang="prolog" inline>?- add(s(s(0)), s(s(0)), s(s(s(s(s(0))))))</syntaxhighlight> fails. In the satisfiability semantics, the failure of the goal means that the truth value of the goal is false. But in the logical consequence semantics, the failure means that the truth value of the goal is unknown.