The Resolution Inference Rule
Substitutions
A substitution θ
is a finite set of the form
{X1/t1,...,Xn/tn}
where each Xi is a distinct variable and each
ti is a term (or more generally, a member of
some given set of objects) not containing Xi.
Each element Xi/ti is called
a binding for Xi.
θ may be applied to an formula
F to obtain Fθ,
the expression obtained from F by similtaneously replacing each
occurrence of the Xis in F by
ti.
Similarly Sθ may be
obtained from a set S of formulae.
A substitution can be applied to another substitution to form their
composition.
Let θ =
{X1/t1,...,Xn/tn}
and σ =
{Y1/s1,...,Yn/sn}
The variables Xi must be distinct from the variables
Yi, and no Xi can appear
in a si.
The composition
θσ
is formed by applying σ to
the ti, and combining the two sets.
For example, let
θ = {P1/jim,P2/brother_of(P4)}
and
σ = {P3/brother_of(P5),P4/geoff}.
Then
θσ =
{P1/jim,P2/brother_of(geoff),P3/brother_of(P5),P4/geoff}.
Unification
A substitution θ unifies
a set S of expressions if
Sθ is a singleton.
A unifier θ is a most general
unifier (mgu) for a set S if for each unifier
σ of S, there exists
a sustitution γ such that
σ =
θγ.
We are interested in substitutions that unify expressions.
Example
|
---|
U = { wise(X),
wise(brother_of(Y)),
wise(brother_of(Z)) }
is unified by θ = {X/brother_of(Z),Y/Z}.
|
The disagreement set of a set S of expressions is defined as
follows :
Locate the left most symbol position at which not all expressions in
S have the same symbol and extract from each expression
in S the subexpression beginning at that symbol position.
The set of all such subexpressions is called the disagreement set.
Example
|
---|
U = { wise(X),
wise(brother_of(Y)),
wise(brother_of(Z)) }
has the disagreement set D = {X,brother_of(Y),brother_of(Z)}
|
Unification algorithm for a set U.
- Put k=0 and
θ0={}
- If Uθk is a singleton
then θk is a mgu for
U.
Otherwise find the disagreement set Dk of
Uθk.
- If there exist variable V and term t
in Dk such that V does not
occur in t, then put
θk+1 =
θk{V/t}, increment
k and loop.
Otherwise stop with failure.
Example
|
---|
U = { wise(X),
wise(brother_of(Y)),
wise(brother_of(Z)) }
k
|
θk
|
Uθk
|
Dk
|
0
|
{}
|
{wise(X),
wise(brother_of(Y)),
wise(brother_of(Z))}
|
{X,
brother_of(Y),
brother_of(Z)}
|
1
|
{X/brother_of(Y)}
|
{wise(brother_of(Y)),
wise(brother_of(Z))}
|
{Y,
Z}
|
2
|
{X/brother_of(Z),
Y/Z}
|
{wise(brother_of(Z))}
|
|
|
Examples
|
---|
U
|
Result
|
{p(X,f(cat)),
p(f(Y),f(Y)),
p(f(Z),T)}
|
{X/f(cat),Y/cat,T/f(cat),Z/cat}
|
{p(X,f(cat)),
p(f(Y),f(Y)),
p(f(dog),Z)}
|
Failure
|
{p(f(Y),f(Y)),
p(f(Z),Z)}
|
Occur check failure
|
|
The occur check is omitted in most Prolog implementations.
Resolution
Propositional binary resolution
C| | L
| +
| D| | ~L
|
|
»
| C| | D|
|
Example
|
---|
i_am_clever | i_will_pass
|
+
|
~i_am_clever | i_am_happy
|
C| = i_will_pass
L = i_am_clever
|
|
D| = i_am_happy
~L = ~i_am_clever
|
C| | D|
|
=
|
i_will_pass | i_am_happy
|
|
An intuitive view of binary resolution is as an implementation of
modus ponens and modus tolens.
Full resolution generalizes the notion.
Propositional full resolution
C| | L1 | ... | Ln
| +
| D| | ~L1 | ... | ~Lm
|
|
»
| C| | D|
|
Example
|
---|
i_am_clever | i_will_pass | i_am_clever
|
+
|
~i_am_clever | i_am_happy
|
C| = i_will_pass
Li = i_am_clever
|
|
D| = i_am_happy
~Li = ~i_am_clever
|
C| | D|
|
=
|
i_will_pass | i_am_happy
|
|
Binary resolution
When performing resolution (and other inference steps) with formulae
that contain variables, it is necessary to rename variables such that
no variables are common across the two clauses.
C| | L
| +
| D| | ~M
|
| Lθ ≡ Mθ
|
|
» |
(C| | D|)θ
|
The two parent clauses resolved against one another, upon the literals
that unify.
The result is a resolvant.
If no literals remain after resolution, the resolvant is FALSE
(indicating that the parent clauses contradicted each other).
There may be multiple possible resolvant of a pair of parents, by selecting
different pairs of literals to resolve upon.
Example
|
---|
~wise(Z) | wise(brother_of(Z))
|
+
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
1st option
|
C| = ~wise(Z)
L = wise(brother_of(Z))
|
|
D| = ~wise(brother_of(Y)) | taller(X,Y)
~M = ~wise(X)
|
θ = {X/brother_of(Z)}
|
C|θ = ~wise(Z)
Lθ = wise(brother_of(Z))
|
|
D|θ = ~wise(brother_of(Y)) | taller(brother_of(Z),Y)
Mθ = wise(brother_of(Z))
|
(C| | D|)θ
|
=
|
~wise(Z) | ~wise(brother_of(Y)) | taller(brother_of(Z),Y)
|
2nd option
|
C| = ~wise(Z)
L = wise(brother_of(Z))
|
|
D| = ~wise(X) | taller(X,Y)
~M = ~wise(brother_of(Y))
|
θ = {Y/Z}
|
D|θ = ~wise(X) | taller(X,Z)
Lθ = wise(brother_of(Z))
|
|
Mθ = wise(brother_of(Z))
C|θ = ~wise(Z)
|
(C| | D|)θ
|
=
|
~wise(Z) | ~wise(X) | taller(X,Z)
|
|
Full resolution
C| | L1 |...| Ln
| +
| D| | ~M1 |...| ~Mm
|
| Liθ ≡ Mjθ
|
| »
| (C| | D|)θ
|
There may be multiple possible resolvant of a pair of parents, by selecting
different combinations of literals to resolve upon.
Example
|
---|
~wise(Z) | wise(brother_of(Z))
|
+
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
1st option - See binary resolution 1st option
|
2nd option - See binary resolution 2nd option
|
3rd option
|
C| = ~wise(Z)
|
|
D| = taller(X,Y)
|
L1 = wise(brother_of(Z))
|
|
~M1 = ~wise(X)
~M2 = ~wise(brother_of(Y))
|
θ = {X/brother_of(Z),Y/Z}
|
C|θ = ~wise(Z)
|
|
D|θ = taller(brother_of(Z),Z)
|
L1θ = wise(brother_of(Z))
|
|
M1θ = wise(brother_of(Z))
M2θ = wise(brother_of(Z))
|
(C| | D|)θ
|
=
|
~wise(Z) | taller(brother_of(Z),Z)
|
|
Example
|
---|
wise(brother_of(geoff)) | wise(Z)
|
+
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
1st option
|
L1 = wise(brother_of(geoff))
|
|
~M1 = ~wise(X)
|
θ = {X/brother_of(geoff)}
|
|
» |
wise(Z) | ~wise(brother_of(Y)) | taller(brother_of(geoff),Y)
|
2nd option
|
L1 = wise(brother_of(geoff))
|
|
~M1 = ~wise(brother_of(Y))
|
θ = {Y/geoff}
|
|
» |
wise(Z) | ~wise(X) | taller(X,geoff)
|
3rd option
|
L1 = wise(brother_of(geoff))
|
|
~M1 = ~wise(X)
~M2 = ~wise(brother_of(Y))
|
θ = {X/brother_of(geoff),Y/geoff}
|
|
» |
wise(Z) | taller(brother_of(geoff),geoff)
|
4th option
|
L1 = wise(Z)
|
|
~M1 = ~wise(X)
|
θ = {Z/X}
|
|
» |
wise(brother_of(geoff)) | ~wise(brother_of(Y)) | taller(X,Y)
|
5th option
|
L1 = wise(Z)
|
|
~M1 = ~wise(brother_of(Y))
|
θ = {Z/brother_of(Y)}
|
|
» |
wise(brother_of(geoff)) | ~wise(X) | taller(X,Y)
|
6th option
|
L1 = wise(Z)
|
|
~M1 = ~wise(X)
~M2 = ~wise(brother_of(Y))
|
θ = {Z/brother_of(Y),X/brother_of(Y)}
|
|
» |
wise(brother_of(geoff)) | taller(brother_of(Y),Y)
|
7th option
|
L1 = wise(brother_of(geoff))
L2 = wise(Z)
|
|
~M1 = ~wise(X)
|
θ = {Z/brother_of(geoff),X/brother_of(geoff)}
|
|
» |
~wise(brother_of(Y)) | taller(brother_of(geoff),Y)
|
8th option
|
L1 = wise(brother_of(geoff))
L2 = wise(Z)
|
|
~M1 = ~wise(brother_of(Y))
|
θ = {Z/brother_of(geoff),Y/geoff}
|
|
» |
~wise(X) | taller(X,geoff)
|
9th option
|
L1 = wise(brother_of(geoff))
L2 = wise(Z)
|
|
~M1 = ~wise(brother_of(Y))
~M2 = ~wise(brother_of(Y))
|
θ = {Z/brother_of(geoff),X/brother_of(geoff),Y/geoff}
|
|
» |
taller(brother_of(geoff),geoff)
|
|
Exercise
Find all possible resolvants of
p(X) | p(f(Y)) | q(X,Y)
and
~p(f(a)) | ~p(X) | ~q(c,d)
Answer
Resolution is a sound inference rule
If a set S of clauses is Herbrand satisfiable, then S ∪
{a resolvant from S} is also Herbrand satisfiable.
(Or, equivalently, if a set S ∪ {a resolvant from S} of clauses
is Herbrand unsatisfiable, then S is Herbrand unsatisfiable.)
Proof
|
---|
Let C| | L1 |...| Ln and
D| | ~M1 |...| ~Mk be
two clauses in a Herbrand satisfiable set of clauses S by the Herbrand
model H, such that the
Lis and Mjs are unifiable
with most general unifier θ, i.e.
the clauses resolve to produce
(C| | D|)θ.
Let σ be any Herbrand universe
substitution so that
(C| | D|)θσ is ground,
and γ any Herbrand universe
substitution so that
(C| | L1 |...| Ln)θσγ
and
(D| | ~M1 |...| ~Mk)θσγ are ground.
(C| | L1 |...| Ln)θσγ
and
(D| | ~M1 |...| ~Mk)θσγ
are TRUE in H.
- If C|θσγ is
TRUE in H then
(C| | D|)θσγ
is TRUE in H.
- If some Liθσγ is
TRUE in H, then all
Liθσγ are
TRUE in H, and all
~Miθσγ are
FALSE in H.
Then D|θσγ must be
TRUE in H and hence
(C| | D|)θσγ
is TRUE in H.
As σ
and γ are arbitary, the resolvant
(C| | D|)θ,
is TRUE in H, i.e.,
S ∪ (C| | D|)θ is satisfiable.
|
Example
|
---|
Consider the resolution between the following two clauses, selected from
a Herbrand satisfiable set S.
Let H be a Herbrand model of S (e.g., the positive or negative interpretation).
~wise(Z) | wise(brother_of(Z))
|
+
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
C| = ~wise(Z)
|
|
D| = taller(X,Y)
|
L1 = wise(brother_of(Z))
|
|
~M1 = ~wise(X)
~M2 = ~wise(brother_of(Y))
|
θ = {X/brother_of(Z),Y/Z}
|
(C| | D|)θ
|
=
|
~wise(Z) | taller(brother_of(Z),Z)
|
One possible σ is
{Z/jim}, and
γ can be {}.
Applying θσγ to the
two clauses gives:
(C| | L1)θσγ =
~wise(jim) | wise(brother_of(jim))
(D| | ~M1 | ~M2)θσγ =
~wise(brother_of(jim)) | ~wise(brother_of(jim)) | taller(brother_of(jim),jim)
which are both TRUE in H.
If C|θσγ = ~wise(jim) is
TRUE in H then
(C| | D|)θσγ =
taller(brother_of(jim),jim) | ~wise(jim) is TRUE in H.
If L1θσγ =
wise(brother_of(jim)) is TRUE in H then
~M1θσγ =
~M2θσγ =
~wise(brother_of(jim)) is FALSE in H and
D|θσγ =
taller(brother_of(jim),jim) must be TRUE in H.
Hence
(C| | D|)θσγ =
taller(brother_of(jim),jim) | ~wise(jim) is TRUE in H.
As σ and
γ are arbitary
(C| | D|)θ =
taller(brother_of(Z),Z) | ~wise(Z) is TRUE in H.
|
This theorem shows that all models of S are models of the resolvant.
In other words, resolvants are logical consequences of the set.
If S ∪ {a resolvant from S} is Herbrand unsatisfiable then
the S is Herbrand unsatisfiable.
An empty clause is derived from a contradictory pair of clauses, and
the existence of such a constradictory pair means that the set cannot have
any model, i.e., the set is (Herbrand) unsatisfiable.
The Quest for Logical Consequence
To show that C is a logical consequence of A, it is necessary to:
- Show that every model of A is a model of C
OR
- Show that S' = A ∪ {~C} is unsatisfiable.
S' is unsatisfiable iff S = CNF(S') is unsatisfiable
- Show that S is unsatisfiable.
A set of clauses has a model iff it has a Herbrand model, so
- Show that S is Herbrand unsatisfiable.
If a set S ∪ {a resolvant from S} of clauses
is Herbrand unsatisfiable, then S is Herbrand unsatisfiable, so
- Do resolution and hope an obviously unsatisfiable set is produced, e.g.,
one containing FALSE
Factoring
Example (showing that binary resolution is not refutation complete)
|
---|
S = { p(X) | q(Y) | q(X)
~q(a) | ~q(Z),
~p(a) }
Full resolution
|
p(X) | q(Y) | q(X)
|
+
|
~q(a) | ~q(Z)
|
» |
p(a)
|
~p(a)
|
+
|
p(a)
|
» |
FALSE
|
Binary resolution
|
Try it, and fail
|
|
The Factoring Inference Rule
C| | L1 |...|Ln
| +
| Factoring
|
| Liθ =
Ljθ
|
| »
| (C| | L1)θ
|
Example
|
---|
~wise(X) | ~wise(brother_of(Y)) |
taller(X,Y) | ~wise(brother_of(jim))
|
1st option
|
C| = ~wise(X) | taller(X,Y)
L1 = ~wise(brother_of(Y))
L2 = ~wise(brother_of(jim))
|
+
|
θ = {Y/jim}
|
|
» |
~wise(X) | taller(X,jim) | ~wise(brother_of(jim))
|
2nd option
|
C| = ~wise(brother_of(Y)) | taller(X,Y)
L1 = ~wise(X)
L2 = ~wise(brother_of(jim))
|
+
|
θ = {X/brother_of(jim)}
|
|
» |
~wise(brother_of(Y)) | taller(brother_of(jim),Y) | ~wise(brother_of(jim))
|
3rd option
|
C| = ~wise(brother_of(jim)) | taller(X,Y)
L1 = ~wise(X)
L2 = ~wise(brother_of(Y))
|
+
|
θ = {X/brother_of(Y)}
|
|
» |
~wise(brother_of(jim)) | taller(brother_of(Y),Y) | ~wise(brother_of(Y))
|
4th option
|
C| = taller(X,Y)
L1 = ~wise(X)
L2 = ~wise(brother_of(Y))
L3 = ~wise(brother_of(jim))
|
+
|
θ = {X/brother_of(jim), Y/jim}
|
|
» |
taller(brother_of(jim),jim) | ~wise(brother_of(jim))
|
|
Factoring is used in conjunction with binary resolution to produce
full resolution.
Example
|
---|
Full resolution
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
+
|
~wise(Z) | wise(brother_of(Z))
|
|
» |
taller(brother_of(Y),Y) | ~wise(Y)
|
Factoring and Binary resolution
|
~wise(X) | ~wise(brother_of(Y)) | taller(X,Y)
|
+
|
Factoring
|
|
» |
~wise(brother_of(Y)) | taller(brother_of(Y),Y)
|
~wise(brother_of(Y)) | taller(brother_of(Y),Y)
|
+
|
~wise(Z) | wise(brother_of(Z))
|
|
» |
taller(brother_of(Y),Y) | ~wise(Y)
|
|
All full resolvants of two clauses are formed from all binary resolvants
of the two clauses, and all binary resolvants of all factors of the two
clauses.
Some resolution strategies are complete using binary resolution and factoring,
with the application of factoring restricted to certain clauses.
This format produces a smaller search space than using full resolution (which
in effect allows factoring on all clauses).
Exam Style Questions
- What is the most general unifier of the following atoms:
p(X,f(Y),Z)
p(T,T,g(cat))
p(f(dog),S,g(W))
- What is the disagreement set of the following atoms:
p(X,f(Y),Z)
p(T,T,g(cat))
p(f(dog),S,g(W))
- List all the binary resolvants of the following two clauses:
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)
- List all the resolvants of the following two clauses:
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)
- List all the factors of the following clause:
p(X,f(Y),Z) | ~s(Z,T) | p(T,T,g(cat)) | p(f(dog),S,g(W)) | ~s(small,hamster)
- One resolvant of the clauses:
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T)
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster)
is
r(f(dog),f(dog)) | ~s(g(cat),f(dog)) | s(big,rat) | ~s(small,hamster)
Show how that may be formed by factoring and binary resolution.
- Prove that if a set S of clauses is Herbrand satisfiable, then
S ∪ {a resolvant from S} is also Herbrand satisfiable
- Use resolution to derive the empty clause from the set
S = { ~p(X) | ~p(f(X)),
p(f(X)) | p(X)
~p(X) | p(f(X)) }