COMP4418: Knowledge Representation
and Reasoning
Resolution
Maurice Pagnucco
School of Computer Science and Engineering
COMP4418, Week 2
1
Goal
Deductive reasoning in language as close as possible to full FOL
¬, ∧, ∨, ∃, ∀
Knowledge Level:
given KB, α, determine if KB |= α
or given an open α(x1 , x2 , . . . xn ), find t1 , t2 , . . . tn
such that KB |= α(t1 , t2 , . . . tn )
When KB is finite {α1 , α2 , . . . , αk }
KB |= α
iff |= [{α1 ∧ α2 ∧ . . . ∧ αk } → α]
iff KB ∪{¬α} is unsatisfiable
iff KB ∪{¬α} |= FALSE
So want a procedure to test for validity, or satisfiability, or for entailing FALSE.
B&L (2005)
2
Clausal Representation
Formula = set of clauses
Clause = set of literals
Literal = atomic sentence or it’s negation
positive literal and negative literal
positive predicate and negative predicate in FOL
Notation:
• If p is a literal, then p̄ is its complement
p̄ ⇒ ¬p ¬p¯ ⇒p
• To distinguish clauses from formulas:
◦ [ and ] for clauses: [p, ¬r , s]
◦ { and } for formulas: {[p, ¬r , s], [p, r , s], [¬p]}
[] is the empty clause; {} is the empty formula
So {} is different from {[]}!
Interpretation:
• Formula understood as conjunction of clauses
• Clause understood as disjunction of clauses
• Literals understood normally
So:
• {[p, ¬q], [r ], s]} is a representation of ((p ∨ ¬q) ∧ r ∧ s)
• [] is a representation of FALSE
• {} is a representation of TRUE
B&L (2005)
3
Resolution Rule of Inference
Given two clauses, infer a new clause:
From clause {p} ∪ C1
and {¬p} ∪ C2 ,
infer clause C1 ∪ C2 .
C1 ∪ C2 is called a resolvent of input clauses with respect to p.
Example:
From clauses [w, p, q] and [w, s, ¬p], have [w, q, s] as resolvent wrt p.
Special Case:
[p] and [¬p] resolve to []
C1 and C2 are empty
A derivation of a clause c from a set S of clauses is a sequence c1 , c2 , . . . , cn of
clauses, where the last clause cn = c, and for each ci , either
1. ci ∈ S, or
2. ci is a resolvent of two earlier clauses in the derivation
Write: S ` c if there is a derivation
B&L (2005)
4
Resolution Rule of Inference
• Generalised Resolution Rule:
For clauses χ ∨ Φ and ¬Ψ ∨ ζ
χ∨Φ ¬Ψ ∨ ζ
l ,
l ,
l ,
l ,
l ,
l ,
l ,
l,
(χ ∨ ζ).θ
• Where θ is a unifier for atomic formulae Φ and Ψ
• χ ∨ ζ is known as the resolvent
5
Rationale
Resolution is a symbol-level rule of inference, but has a connection to
knowledge-level logical interpretations
Resolvent is entailed by input clauses
Suppose I |= (p ∨ α) and I |= (¬p ∨ β)
Case 1: I |= p
then I |= β, so I |= (α ∨ β).
Case 2: I 2 p
then I |= α, so I |= (α ∨ β).
Either way, I |= (α ∨ β).
So: {(p ∨ α), (¬p ∨ β)} |= (α ∨ β).
Special case:
[p] and [¬p] resolve to [],
so {[p], [¬p]} |= FALSE
that is: {[p], [¬p]} is unsatisfiable
B&L (2005)
6
Derivations and entailment
Can extend the previous argument to derivations:
If S ` c then S |= c
Proof: by induction on the length of the derivation.
Show (by looking at the two cases) that S |= ci .
But the converse does not hold in general
Can have S |= c without having S ` c.
Example: {[¬p]} |= [¬p, ¬q], i.e., ¬p |= (¬p ∨ ¬q)
but no derivation
However, . . .
Resolution is sound and complete for [] !
Theorem: S ` [] iff S |= []
Result will carry over to quantified clauses (later)
So for any set S of clauses:
S is unsatisfiable iff S ` [].
Provides method for determining satisfiability:
Search all derivations to see if [] is produced
Also provides method for determining all entailments
B&L (2005)
7
Example
KB:
∀x GradStudent(x) → Student(x)
∀x Student(x) → HardWorker(x)
GradStudent(sue)
Q: HardWorker(sue)
B&L (2005)
8
The 3 block example
KB = {On(a,b), On(b,c), Green(a), ¬Green(c)}
already in CNF
Q = ∃x∃y [On(x,y ) ∧ Green(x) ∧ ¬Green(y )]
Note: ¬Q has no existentials to eliminate;
yields {[¬On(x,y), ¬Green(x), Green(y )]} in CNF
B&L (2005)
9
Arithmetic
KB:
Plus(zero,x,x)
Plus(x,y ,z) → Plus(succ(x),y ,succ(z))
Q: ∃u Plus(2,3,u)
where for readability, we use
0 for zero,
3 for succ(succ(succ(zero))) etc.
B&L (2005)
10
Answer predicates
In full FOL, have possibility of deriving ∃xP(x) without being able to derive P(t) for any t
e.g. the three-blocks problem
∃x∃y [On(x,y ) ∧ Green(x) ∧ ¬Green(y )]
but cannot derive which block is which
Solution: answer-extraction process
replace query ∃xP(x) by ∃x[P(x) ∧ ¬A(x)],
where A is a new predicate symbol called the answer predicate
instead of deriving [], derive any clause containing just the answer predicate
can always convert a derivation of []
Example KB: {Student(john), Student(jane), Happy(john)}
Q: ∃x [Student(x) ∧ Happy(x)]
B&L (2005)
11
Disjunctive answers
Example KB: {Student(john), Student(jane), [Happy(john) ∨ Happy(jane)]}
Q: ∃x [Student(x) ∧ Happy(x)]
Note:
can have variables in answer
need to watch for Skolem symbols . . .
B&L (2005)
12
A Problem
KB: LessThan(succ(x), y) → LessThan(x, y )
Q: LessThan(zero, zero)
Should fail since KB 6|= Q
Infinte branch of resolvents
cannot use a simple depth-first procedure to search for []
B&L (2005)
13
Undecidability
Is there a way to detect when this happens?
No! FOL is very powerful
• can be used as a full programming language
• just as there is no way to detect in general when a program is looping
There can be no procedure that does this:
Proc[Clauses] =
If Clauses are unsatisfiable
then return YES
else return NO
However: Resolution is complete some branch will contain [], for unsat clauses
So breadth-first search guaranteed to find []
search may not terminate on satisfiable clauses
B&L (2005)
14
Overly specific unifiers
In general, no way to guarantee efficiency, or even termination
later: put control into users’ hands
One major way:
reduce redundancy in search, by keeping search as general as possible
Example:
. . . , P(g(x), f (x), z)] [¬P(y, f (w), a), . . .
unified by
θ1 = {x/b, y /g(b), z/a, w/b} gives P(g(b), f (b), a)
and by
θ2 = {x/f (z), y /g(f (z)), z/a, w/f (z)} gives P(g(f (z)), f (f (z)), a).
Might not be able to derive [] from clauses having overly specific substitutions
wastes time in search!
B&L (2005)
15
Most general unifiers
θ is a most general unifier of literals l1 and l2 iff
1. θ unifies l1 and l2
2. for any other unifier θ0 , there is another substitution θ∗ such that θ0 = θθ∗
note: composition θθ∗ requires applying θ∗ to terms in θ
for previous example, an MGU is
θ = {x/w, y/g(w), z/a}
for which
θ1 = θ{w/b}
θ2 = θ{w/f (z)}
Theorem: Can limit search to MGUs only without loss of completeness (with certain caveats)
Computing an MGU, given a set of lits {li }
1. Start with θ = {}.
2. If all the li θ are identical, then done; otherwise, get disagreement set, DS
e.g. P(a, f (a, g(z), . . . P(a, f (a, u, . . . disagreement set, DS = {u, g(z)}
3. Find a variable v ∈ DS, and a term t ∈ DS not containing v . If not, fail.
4. θ = θ{v /t}
5. Go to 2
Note: there is a better linear algorithm
B&L (2005)
16
Herbrand Theorem
Some 1st-order cases can be handled by converting them to a propositional form
Given a set of clauses S
• the Herbrand universe of S is the set of all terms formed using only the function symbols (and
constants, at least one) in S
for example, if S uses (unary) f , and c, d,
U = {c, d, f (c), f (d), f (f (c)), f (f (d)), f (f (f (c))), . . .}
• the Herbrand base of S is
{cθ|c ∈ S and θ replaces the variables in c by terms from the Herbrand universe}
Theorem: S is satisfiable iff Herbrand base is (applies to Horn clauses also)
Herbrand base has no variables, and so is essentially propositional, though usually infinite
• finite, when Herbrand universe is finite
can use propositional methods (guaranteed to terminate)
• sometimes other “type” restrictions can be used to keep the Herbrand base finite
include f (t) only if t is the correct type
B&L (2005)
17
Resolution is difficult!
First-order resolution is not guaranteed to terminate.
What can be said about the propositional case?
• Recently shown by Haken that there are unsatisfiable clauses {c1 , c2 , . . . , cn } such that the
shortest derivation of [] contains on the order of 2n clauses
• Even if we could always find a derivation immediately, the most clever search procedure will
still require exponential time on some problems
Problem just with resolution?
• Probably not.
• Determining if set of clauses is satisfiable shown by Cook to be NP-complete
◦ no easier than an extremely large variety of computational tasks
◦ any search task where what is searched for can be verified in polynomial time can be
recast as a satisfiability problem
satisfiability
does graph of cities allow for a full tour of size k miles?
can N queens be put on an N × N chessboard all safely?
...
• Satisfiability is strongly believed
B&L (2005)
18
Implications for KR
Problem: want to produce entailments of KB as needed for immediate action
• full theorem-proving may be too difficult for KR!
• need to consider other options
giving control to user
procedural representations (later)
less expressive languages
e.g. Horn clauses (and a major theme later)
In some applications, it is reasonable to wait
• e.g. mathematical theorem proving, where we only care about specific formula
Best to hope for in general: reduce redundancy
• refinements to resolution to improve search
Main example: MGU, as before
• but many other possibilities
need to be careful to preserve completeness
• ATP: automated theorem proving
area that studies strategies for proving difficult theorems
main application: mathematics, but relevance also to KR
B&L (2005)
19
Strategies
1. Clause elimination
• pure clause
contains literal l such that ¬l does not appear in any other clause
clause cannot lead to []
• tautology
clause with a literal and its negation
any path to [] can bypass tautology
• subsumed clause
a clause such that one with a subset of its literals is already present
path to [] need only pass through short clause
can be generalized to allow substitutions
2. Ordering strategies
many possible ways to order search, but best and simplest is
• unit preference
prefer to resolve unit clauses first
Why? Given unit clause and another clause, resolvent is a smaller one ← []
B&L (2005)
20
Strategies 2
3. Set of support
• KB is usually satisfiable, so not very useful to resolve among clauses with only ancestors in KB
• contradiction arises from interaction with ¬Q
• always resolve with at least one clause that has an ancestor in ¬Q
• preserves completeness (sometimes)
4. Connection graph
• pre-compute all possible unifications
• build a graph with edges between any two unifiable literals of opposite polarity
label edge with MGU
• Resolution procedure:
repeatedly:
select link
compute resolvent
inherit links from parents after substitution
• Resolution as search:
find sequence of links L1 , L2 , . . . producing []
B&L (2005)
21
Strategies 3
5. Special treatment for equality
• instead of using axioms for =, relexitivity, symmetry, transitivity, substitution of equals for equals
• use new inference rule: paramodulation
• from {(t = s)} ∪ C1 and {P(. . . t 0 . . .)} ∪ C2 where tθ = t 0 θ
• infer {P(. . . s . . .)}θ ∪ C1 θ ∪ C2 θ.
• collapses many resolution steps into one; see also: theory resolution (later)
6. Sorted logic
• terms get sorts:
x:Male mother:[Person → Female]
• keep taxonomy of sorts
• refuse to unify P(s) with P(t) unless sorts are compatible
• assumes only “meaningful” paths will lead to []
B&L (2005)
22
Finally . . .
7. Directional connectives
• given [¬p, q], can interpret as either
from p, infer q (forward)
to prove q, prove p (backward)
procedural reading of →
• In 1st case:
would only resolve [¬p, q] with [p,. . . ] producing [q,. . . ]
• In 2nd case:
would only resolve [¬p, q] with [¬q,. . . ] producing [¬p,. . . ]
• Intended application:
forward: Battleship(x) → Gray(x)
do not want to try to prove something is gray by proving it is a battleship
backward: Human(x) → Has(x,spleen)
do not want to conclude from someone being human,
that she has each property
• the basis for the procedural representations
B&L (2005)
23