76
Formal Logic
Universal quantifiers are not explicitly part of the rule as it appears in a Prolog
program, but Prolog treats the rule as being universally quantified
(4y)(4x)[E( y, x) ` A(x) S Pr(x)]
and repeatedly uses universal instantiation to strip off the universal quantifiers
and allow the variables to assume in turn each value of the domain.
Both facts and rules are examples of Horn clauses. A horn clause is a wff
composed of predicates or the negations of predicates (with either variables or
constants as arguments) joined by disjunctions, where at most one predicate is
unnegated. Thus the fact
E(d, g)
is an example of a Horn clause because it consists of a single unnegated predicate.
The wff
[E( y, x)]′ ~ [A(x)]′ ~ Pr(x)
is an example of a Horn clause because it consists of three predicates joined by
disjunction where only Pr(x) is unnegated. By De Morgan’s law, it is equivalent to
[E( y, x) ` A(x)]′ ~ Pr(x)
which in turn is equivalent to
E( y, x) ` A(x) S Pr(x)
and therefore represents the rule in our Prolog program.
The single rule of inference used by Prolog is called resolution. Two Horn
clauses in a Prolog database are resolved into a single new Horn clause if one
contains an unnegated predicate that matches a negated predicate in the other
clause. The new clause eliminates the matching term and is then available to use
in answering the query. For example,
A(a)
[A(a)]′ ~ B(b)
resolves to B(b). This says that from
A(a), [A(a)]′ ~ B(b)
which is equivalent to
A(a), A(a) S B(b)
Prolog infers
B(b)
ReMIndeR
Prolog’s resolution rule
looks for a term and its
negation to infer one Horn
clause from two.