COMP30026 Models of Computation – Predicate Logic: Unification and Resolution
COMP30026 Models of Computation
Predicate Logic: Unification and Resolution
Bach Le / Anna Kalenkova
Lecture Week 5 Part 1 (Zoom)
Semester 2, 2021
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 1 / 32
This Lecture is Being Recorded
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 2 / 32
Notation for Variables and Constants
Recall again our convention: We use letters from the start of the
alphabet (a, b, c, . . . ) for constants, and letters from the end of the
alphabet (u, v , x , y . . . ) for variables.
This distinction is very important in what follows.
We also usually use lower case letters such as f , g , h, . . . as function
symbols, and, of course, upper case letters for predicate symbols.
In some contexts it is important to distinguish function symbols and
predicate symbols. As far as unification is concerned, however, there
is no difference—the unification algorithm treats f (x , a) and
P(f (x , a), x) the same way, so for now, let us just consider both
“terms”.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 3 / 32
Substitutions
A substitution is a finite set of replacements of variables by terms,
that is, a set θ of the form {x1 7→ t1, x2 7→ t2, . . . , xn 7→ tn}, where
the xi are variables and the ti are terms.
We can also think of θ as a function from terms to terms, or from
atomic formulas to atomic formulas. θ(F ) is the result of
simultaneously replacing each occurrence of xi in F by ti .
Example: If F is P(f (x), g(y , y , b)), and
θ = {x 7→ h(u), y 7→ a, z 7→ c} then θ(F ) is P(f (h(u)), g(a, a, b)}.
Note: Similar to a valuation, but a substitution maps a variable to a
term, and, by natural extension, terms to terms.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 4 / 32
Most General Unifiers
A unifier of two terms s and t is a substitution θ such that
θ(s) = θ(t).
The terms s and t are unifiable iff there exists a unifier for s and t.
A most general unifier (mgu) for s and t is a substitution θ such that
1 θ is a unifier for s and t, and
2 every other unifier σ of s and t can be expressed as τ ◦ θ for
some substitution τ .
(The composition τ ◦ θ is the substitution we get by first using θ, and
then using τ on the result produced by θ.)
Theorem. If s and t are unifiable, they have a most general unifier.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 5 / 32
Unifier Examples
1 P(x , a) and P(b, c) are not unifiable.
2 P(f (x), y ) and P(a,w) are not unifiable.
3 P(x , c) and P(a, y ) are unifiable using {x 7→ a, y 7→ c}.
4 P(f (x), c) and P(f (a), y ) also unifiable using {x 7→ a, y 7→ c}.
5 Note: P(x) and P(f (x)) are not unifiable.
The last case relies on a principle that a variable (such as x) is not
unifiable with any term containing x (apart from x itself).
If we were allowed to have a substitution {x 7→ f (f (f (. . .)))}, that
would be a unifier for the last example. But we cannot have that, as
terms must be finite.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 6 / 32
More Unifier Examples
Now consider P(f (x), g(y , a)) and P(f (a), g(z , a)).
The following are all unifiers, so which is “best”?
{x 7→ a, y 7→ z}
{x 7→ a, y 7→ a, z 7→ a}
{x 7→ a, y 7→ g(b, f (u)), z 7→ g(b, f (u))}
{x 7→ a, z 7→ y}
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 7 / 32
More Unifier Examples
Now consider P(f (x), g(y , a)) and P(f (a), g(z , a)).
The following are all unifiers, so which is “best”?
{x 7→ a, y 7→ z}
{x 7→ a, y 7→ a, z 7→ a}
{x 7→ a, y 7→ g(b, f (u)), z 7→ g(b, f (u))}
{x 7→ a, z 7→ y}
The first and the last are mgus. They avoid making unnecessary
commitments. The second commits y and z to take the value a,
which was not really needed in order to unify the two formulas.
Note that {x 7→ a, y 7→ a, z 7→ a} = {z 7→ a} ◦ {x 7→ a, y 7→ z}.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 7 / 32
A Unification Algorithm
In the following, let x be a variable, let F and G be function or
predicate names, and let s and t be arbitrary terms.
Input: Two terms s and t.
Output: If they are unifiable: a most general unifier for s and t;
otherwise ‘failure’.
Algorithm: Start with the set of equations {s = t}.
(This is a singleton set: it has one element.)
As long as some equation in the set has one of the six forms listed on
the next slide, perform the corresponding action.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 8 / 32
Unification: Solving Term Equations
1. F (s1, . . . , sn) = F (t1, . . . , tn):
• Replace the equation by the n equations s1 = t1, . . . , sn = tn.
2. F (s1, . . . , sn) = G (t1, . . . , tm) where F 6= G or n 6= m:
• Halt, returning ‘failure’.
3. x = x :
• Delete the equation.
4. t = x where t is not a variable:
• Replace the equation by x = t.
5. x = t where t is not x but x occurs in t:
• Halt, returning ‘failure’.
6. x = t where t contains no x but x occurs in other equations:
• Replace x by t in those other equations.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 9 / 32
Solving Term Equations: Example 1
Starting from
f (h(y ), g(y , a), z) = f (x , g(v , v ), b)
we rewrite:
(1,4)
=⇒
x = h(y )
g(y , a) = g(v , v )
z = b
(1,4)
=⇒
x = h(y )
y = v
v = a
z = b
(6,6)
=⇒
x = h(a)
y = a
v = a
z = b
The last set is in normal form and corresponds to the substitution
θ = {x 7→ h(a), y 7→ a, v 7→ a, z 7→ b}
which indeed unifies the two original terms.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 10 / 32
Solving Term Equations: Example 2
Starting from
f (x , a, x) = f (h(z , b), y , h(z , y ))
we rewrite:
(1,4)
=⇒
x = h(z , b)
y = a
x = h(z , y )
(6)
=⇒
x = h(z , b)
y = a
h(z , b) = h(z , y )
(1,4)
=⇒
x = h(z , b)
y = a
z = z
y = b
(3)
=⇒
x = h(z , b)
y = a
y = b
(6)
=⇒
x = h(z , b)
y = a
a = b
(2)
=⇒ failure
So the two original terms are not unifiable.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 11 / 32
Solving Term Equations: Example 3
Starting from
f (x , g(v , v ), x) = f (h(y ), g(y , z), z)
we rewrite:
(1)
=⇒
x = h(y )
g(v , v ) = g(y , z)
x = z
(6,4)
=⇒
x = h(y )
g(v , v ) = g(y , z)
z = h(y )
(1)
=⇒
x = h(y )
v = y
v = z
z = h(y )
(6)
=⇒
x = h(y )
z = y
v = z
z = h(y )
(6)
=⇒
x = h(y )
z = y
v = y
y = h(y )
(5)
=⇒ failure
This is “failure by occurs check”: The algorithm fails, as soon as we
discover the equation y = h(y ).
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 12 / 32
Term Equations as Substitutions
The process of solving term equations always halts.
When it halts without reporting ‘failure’, the term equation system is
left in a normal form: On the left-hand sides we have variables only,
and they are all different. Moreover, these variables occur nowhere in
the right-hand sides.
If the normal form is {x1 = t1, . . . , xn = tn} then
{x1 7→ t1, . . . , xn 7→ tn}
is a most general unifier for the input terms s and t.
If the result is ‘failure’, no unifier exists.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 13 / 32
Resolvents
Recall how we defined resolvents for propositional logic:
Two literals are complementary if one is L and the other is ¬L.
The resolvent of two clauses containing complementary literals
L, ¬L is their union omitting L and ¬L.
For predicate logic we have:
Two literals L and ¬L′ are complementary if {L, L′} is unifiable.
Let C1 and C2 be clauses, renamed apart. Let θ be an mgu of
complementary literals {L,¬L′} with L a literal in C1 and ¬L
′ a
literal in C2. Then the resolvent of C1 and C2 is the union
θ(C1 \ {L}) ∪ θ(C2 \ {¬L
′}).
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 14 / 32
Automated Inference with Predicate Logic
Every shark eats a tadpole
∀x(S(x)⇒∃y (T (y ) ∧ E (x , y )))
All large white fish are sharks
∀x(W (x)⇒ S(x))
Colin is a large white fish living in deep water
W (colin) ∧ D(colin)
Any tadpole eaten by a deep water fish is miserable
∀z((T (z) ∧ ∃y (D(y ) ∧ E (y , z)))⇒M(z))
Therefore some tadpole is miserable
∴ ∃z(T (z) ∧M(z))
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 15 / 32
Tadpoles in Clausal Form
Every shark eats a tadpole
• ∀x (S(x)⇒∃y (T (y ) ∧ E (x , y ))) {¬S(x),T (f (x))}
• {¬S(x),E (x , f (x))}
All large white fish are sharks
• ∀x (W (x)⇒ S(x)) {¬W (x), S(x)}
Colin is a large white fish living in deep water
• W (colin) ∧ D(colin) {W (colin)}
• {D(colin)}
Any tadpole eaten by a deep water fish is miserable
• ∀z ((T (z) ∧ ∃y (D(y ) ∧ E (y , z)))⇒M(z))
• {¬T (z),¬D(y ),¬E (y , z),M(z)}
Negation of: Some tadpole is miserable
• ¬∃z (T (z) ∧M(z)) {¬T (z),¬M(z)}
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 16 / 32
A Refutation
Let us find a refutation of the set of seven clauses.
To save space, we leave out braces and some parentheses, for
example, we write ¬Wu, Su for clause {¬W (u), S(u)}.
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Many different resolution proofs are possible—the next slides show
one.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 17 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
A Refutation for the Tadpole Example
¬Wu, Su ¬Sv ,T (fv ) ¬Tz ,¬Dy ,¬E (y , z),Mz
Wc ¬Sx ,E (x , fx) Dc ¬Tw ,¬Mw
Sc ¬Tz ,¬Dy ,¬E (y , z)
E (c, fc) ¬Tz ,¬E (c, z)
¬Sv ,¬E (c, fv )
¬Sc
⊥ —empty clause, so input set unsatisfiable
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 18 / 32
Resolution Exercise
Using resolution, justify this argument:
All philosophers are wise ∀x (P(x)⇒W (x))
Some Greeks are philosophers ∃x (G (x) ∧ P(x))
Therefore some Greeks are wise ∃x (G (x) ∧W (x))
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 19 / 32
Factoring
In addition to resolution, there is one more valid rewriting of clauses,
called factoring.
Let C be a clause and let A1,A2 ∈ C . If A1 and A2 are unifiable with
mgu θ, add the clause θ(C ).
{D(f (y ), y ),¬P(x),D(x , y ),¬P(z)}
{D(f (y ), y ),¬P(f (y )),¬P(z)}
{D(f (y ), y ),¬P(f (y ))}
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 20 / 32
The Need for Factoring
Factoring is sometimes crucial:
{P(x),P(y )} {¬P(u),¬P(v )}
{P(x)} {¬P(u)}
⊥
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 21 / 32
How to Use Clauses
A resolution step uses two clauses (or two “copies” of the same
clause). A factoring step uses one clause.
A given clause can be used many times in a refutation, taking part in
many different resolution/factoring steps.
But recall that each clause is implicitly universally quantified.
Hence we really should rename all variables in a clause every time we
use the clause, using fresh variable names.
Sometimes this renaming is essential for correctness, especially when
resolution uses two “copies” of the same clause.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 22 / 32
Leibniz’s Dream
The only way to rectify our reasonings is to make them as
tangible as those of the Mathematicians, so that we can find
our error at a glance, and when there are disputes among
persons, we can simply say: Let us calculate, without further
ado, to see who is right.
G. W. Leibniz, 1685
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 23 / 32
The Resolution Method
Start with collection C of clauses
While ⊥ 6∈ C do
add to C a factor of some C ∈ C
or a resolvent of some C1,C2 ∈ C
Does this process always terminate?
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 24 / 32
The Power of Resolution
Theorem. C is unsatisfiable iff the resolution method can add ⊥
after a finite number of steps.
We say that resolution is sound and complete.
It gives us a proof procedure for unsatisfiability (and validity).
Note, however, that resolution does not give a decision procedure for
unsatisfiability (or validity) of first-order predicate logic formulas.
Indeed, it can be shown that there are no such proof procedures.
We say that validity and unsatisfiability are semi-decidable)
properties.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 25 / 32
Proof Search
Resolution only works if we apply a sensible search strategy:
{Q} {¬Q} {¬P(x),P(f (x))}
{¬P(x),P(f (f (x)))}
*
{¬P(x),P(f (f (f (x))))}
…
Moreover, search can be expensive.
* Here we used two copies of the same clause for resolution—the
second using fresh variables, say {¬P(y ),P(f (y ))}. When the
resolvent is later used, it too is first renamed.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 26 / 32
Proof Search Strategies
There is a chapter on resolution proofs
on the LMS, under “Readings Online”.
It covers different search strategies, and
it also has a longer explanation of why
resolution is sound and complete.
(For the latter it uses concepts of
Herbrand interpretation and semantic
tree.)
These parts are not examinable.
Jacques Herbrand, 1908–1931
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 27 / 32
Horn Clauses and Prolog
A Horn clause is a clause with at most one positive literal.
All seven clauses used in the tadpole example were Horn.
A clause such as {¬T (z),¬D(y ),¬E (y , z),M(z)} can also be
thought of as
(T (z) ∧ D(y ) ∧ E (y , z))⇒M(z)
In the logic programming language Prolog, the clause is written
miserable(Z) :- tadpole(Z),
deepwaterfish(Y),
eats(Y,Z).
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 28 / 32
Horn Clauses and Search
For logic programs, the restriction to Horn clauses simplifies the
search problem, but it does not remove it.
For propositional Horn clauses, satisfiability can be decided in linear
time. (For arbitrary propositional CNF it is NP-complete.)
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 29 / 32
Sidebar: Unification and Type Inference
Another important use of unification is in type checking/inference.
Here variables are type variables and the function symbols are type
constructors. For example, think of the list type constructor as
‘List’, so we write ‘list(x)’ instead of the Haskell type ‘[x]’, and
let us write ‘fun(x,y)’ instead of ‘x -> y’:
map :: fun(fun(x,y), fun(list(x), list(y)))
null :: fun(list(z), bool)
If we use the expression map null “abc” then the type checker
effectively sets up these equations:
fun(x,y) = fun(list(z), bool) — for map null
list(x) = list(char) — for (map null) “abc”
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 30 / 32
Sidebar: Unification and Type Inference
The unification algorithm then produces these equations:
x = list(z)
y = bool
x = char
and hence
list(z) = char
Unification failure shows that map null “abc” is not well-typed.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 31 / 32
Next Up
Next we’ll look at mathematical proof techniques.
Next week: We establish some basic discrete mathematics concepts
and results: sets, relations and functions.
Models of Computation (Sem 2, 2021) Predicate Logic: Unification and Resolution c© University of Melbourne 32 / 32