Resolution in First
Order Logic
Given clauses C1 and C2, a clause C is a RESOLVENT of C1 and C2,
if
1. There is a subset C1' = {A1, .., Am} of C1 of literals of the
same sign, say
positive, and a subset C2' = {B1, .., Bn} of C2 of literals of the
opposite sign, say
negative,
2. There are substitutions s1 and s2 that replace variables in C1'
and C2' so as to
have new variables,
3. C2'' is obtained from C2 removing the negative signs from B1 ..
Bn
4. There is an Most General Unifier s for the union of C1'.s1 and
C2''.s2
and C is
((C1 - C1').s1 UNION (C2 - C2').s2).s
In symbols this Resolution inference rule becomes:
{C1, C2}
--------
C
If C1' and C2' are singletons (i.e. contain just one literal), the
rule is called Binary
Resolution.
Example:
C1 = {(P z (F z)) (P z A)}
C2 = {(NOT (P z A)) (NOT (P z x)) (NOT (P x z))
C1' = {(P z A)}
C2' = {(NOT (P z A)) (NOT (P z x))}
C2'' = {(P z A) (P z x)}
s1 = [z1/z]
s2 = [z2/z]
C1'.s1 UNION C2'.s2 = {(P z1 A) (P z2 A) (P z2 x)}
s = [z1/z2 A/x]
C = {(NOT (P A z1)) (P z1 (F z1))}
Notice that this application of Resolution has eliminated more
than one literal from C2,
i.e. it is not a binary resolution.
Theorem: First Order Logic, with the Resolution Inference Rule, is
sound and
refutation complete.
We will not develop the proof of this theorem. We will instead
look at some of its steps,
which will give us a wonderful opportunity to revisit Herbrand.
But before that let's
observe that in a sense, if we replace in this theorem
"Resolution" by "Binary
Resolution", then the theorem does not hold and Binary
Resolution is not Refutation
Complete. This is the case when in the implementation we do not
use sets but instead use
bags.This can be shown using the same example as in the case of
propositional logic.
Given a clause C, a subset D of C, and a substitution s that
unifies D, we define C.s to be
a Factor of C.
The Factoring Inference Rule is the rule with premise C and
as consequence C.s.
Theorem: For any set of clauses S and clause C, if C is derivable
from S using
Resolution, then C is derivable from S using Binary Resolution and
Factoring.
When doing proofs it is efficient to have as few clauses as
possible. The following
definition and rule are helpful in eliminating redundant clauses:
A clause C1 Subsumes a clause C2 iff there is a
substitution s such that C1.s is a
subset of C2.
Subsumption Elimination Rule: If C1 subsumes C2 then eliminate C2.
General Method
If A is the Fill-In-Blanks question that we need to answer and x1
.. xn are the free
variables occurring in A, then we add to the Non-Logical axioms
and Facts GAMMA the
clause
NOT A OR ANS(x1 .. xn)
We terminate the proof when we get a clause of the form
ANS(t1 .. tn)
t1 .. tn are terms that denote individuals that simultaneously
satisfy the query for,
respectively x1 .. xn.
We can obtain all the individuals that satisfy the original query
by continuing the proof
looking for alternative instantiations for the variables x1 .. xn.
If we build the proof tree for ANS(t1 .. tn) and consider the MGUs
used in it, the
composition of these substitutions, restricted to x1 .. xn, gives
us the individuals that
answer the original Fill-In-Blanks question.
o (B[t/x] AND C[t/x]) if A is (B AND C), and similarly for the
other
connectives,
o (ALL x B) if A is (ALL x B), (similarly for EXISTS),
o (ALL y B[t/x]), if A is (ALL y B) and y is different from x
(similarly for
EXISTS).
The substitution [t/x] can be seen as a map from terms to terms
and from formulae to
formulae. We can define similarly [t1/x1 t2/x2 .. tn/xn], where t1
t2 .. tn are terms and x1
x2 .. xn are variables, as a map, the [simultaneous]
substitution of x1 by t1, x2 by t2, ..,
of xn by tn. [If all the terms t1 .. tn are variables, the substitution is
called an alphabetic
variant, and if they are ground terms, it is called a ground
substitution.] Note that a
simultaneous substitution is not the same as a sequential
substitution.
No comments:
Post a Comment