Goal
Deductive reasoning in language as close as possible to full FOL
! ! ¬,∧,∨,∃,∀ Knowledge Level:
! ! or!
!
given KB, α, determine if KB |= α.
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 ! iff ! iff !
|=[(α1∧α2∧…∧αk)⊃α] KB∪{¬α}isunsatisfiable KB∪{¬α}|=FALSE
So want a procedure to test for validity, or satisfiability, or for entailing FALSE.
Will now consider such a procedure ! first: without quantifiers
KR & R! © Brachman & Levesque 2005
Resolution
Clausal Representation
Formula = set of clauses
Clause = set of literals
Literal = atomic sentence or its negation ! ! positive literal and negative literal
Notation:
! If l is a literal, then ¬ l 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 literals
! Literals understood normally
So:!
! {[p,¬q], [r], [s]} is representation of ((p ∨ ¬q) ∧ r ∧ s)
! [] is a representation of FALSE
! {} is a representation of TRUE
KR & R! © Brachman & Levesque 2005
Resolution
CNF and DNF
Every propositional wff α can be converted into a formula α′ in Conjunctive Normal Form (CNF) in such a way that |= α≡ α′.
1.!eliminate ⊃and ≡
+ using (α⊃β) ß (¬α∨β) etc.
2.!push ¬ inward
! using ¬(α∧β) ß (¬α∨¬β) etc.
3.!distribute ∨over ∧
+ using ((α∧β) ∨γ) ß ((α∨γ) ∧(β∨γ))
4.!collect terms
! using (α∨α) ß α etc.
Result is a conjunction of disjunction of literals.
! an analogous procedure produces DNF, a disjunction of conjunction of literals
We can identify CNF wffs with clausal formulas
! (p ∨¬q ∨r) ∧ (s∨¬r) ß {[p, ¬q, r], [s, ¬r]} So: given a finite KB and α, to find out if
KB |= α, it will be sufficient to
1.!put (KB ∧ ¬α) into CNF, as above
2.!determine the satisfiability of clauses
KR & R! © Brachman & Levesque 2005
Resolution
Resolution rule of inference
Given two clauses, infer a new clause:
! From clause !
! and! !
! infer clause!
{p} ∪ C1,! {¬p}∪C2,! 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
KR & R! © Brachman & Levesque 2005
Resolution
Rationale
Resolution is a symbol-level rule of inference, but has a connection to knowledge-level logical interpretations
Resolvent is entailed by input clauses.
! SupposeI|= (p∨α)and I|= (¬p∨β) + Case1: I|=p
! ! then I|=β, so I|=(α∨β). + Case2: I|≠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
KR & R! © Brachman & Levesque 2005
Resolution
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 ! CanhaveS|=c withouthaving 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:
! Searchallderivationstoseeif[]isproduced
! Also provides method for determining all entailments
KR & R! © Brachman & Levesque 2005
Resolution
A procedure for entailment
To determine if KB |= α,
• put KB, ¬α into CNF to get S, as before
• checkifS|⎯[].
! If KB = {}, then we are testing the validity of α.
Non-deterministic procedure
1.!
! !
2.!
and c2
!
produce !
! !
Check if [] is in S.
If yes, then return UNSATISFIABLE
Check if there are two clauses c1 in S such that they resolve to
a c3 not already in S.
If no, then return SATISFIABLE Addc3 toSandgoto1.
3.!
Note: need only convert KB to CNF once
• can handle multiple queries with same KB
• after addition of new fact α, can simply add new clauses α′ to KB
KR & R! © Brachman & Levesque 2005
Resolution
Example 1
KB:
! FirstGrade
! FirstGrade ⊃ Child
! Child ∧ Male ⊃ Boy
! Kindergarten ⊃ Child
! Child ∧ Female ⊃ Girl
! Female
Show that KB |= Girl [FirstGrade]
[¬ Child, ¬ Male, Boy]
[Child]
[Girl, ¬ Female]
Derivation has
9 clauses, 4 new
[¬ Kindergarten, Child] [Female]
[¬ FirstGrade, Child]
[¬ Child, ¬ Female, Girl]
[Girl]
[]
[¬ Girl] negation of query
KR & R! © Brachman & Levesque 2005
Resolution
Example 2
KB:
! (Rain ∨Sun)
! (Sun ⊃ Mail)
! ((Rain ∨ Sleet) ⊃ Mail)
Show KB |= Mail
Similarly
KB |≠ Rain
[Rain , Sun]
[Rain]
[¬Sleet, Mail]
[¬Sun, Mail] [¬Rain, Mail] [¬Mail]
[¬Sun]
[]
[¬Rain]
Note: every clause
not in S has 2 parents
! Can enumerate all clauses given ¬ Rain and [] will not be generated
KR & R! © Brachman & Levesque 2005
Resolution
Quantifiers
Clausal form as before, but atom is
! P(t1, t2, …, tn), where ti may contain variables
Interpretation as before, but variables are understood universally
Example: {[P(x), ¬ R(a,f(b,x))], [Q(x,y)]} ! ! interpreted as
+ ∀x∀y{[R(a,f(b,x)) ⊃ P(x)] ∧ Q(x,y)} Substitutions: θ = {v1/t1, v2/t2, …, vn/tn}
Notation: If l is a literal and θ is a substitution, ! then lθ is the result of the substitution
! ! clause)
Example:
(and similarly, cθ where c is a θ = {x/a, y/g(x,b,z)}
P(x,z,f(x,y)) θ = P(a,z,f(a,g(x,b,z)))
A literal is ground if it contains no variables.
A literal l is an instance of l′, if forsomeθ,l=l′θ.
+ +
KR & R! © Brachman & Levesque 2005
Resolution
Generalizing CNF
Resolution will generalize to handling variables
But how to convert wffs to CNF?
Need three additional steps: Ignore = for now 1.!eliminate ⊃and ≡
2.!push ¬ inward
! using also ¬∀x.α ß ∃x.¬α etc.
3.!standardize variables: each quantifier gets its own variable
! e.g. ∃x[P(x)] ∧Q(x) ß ∃z[P(z)] ∧ Q(x)! ! ! variable
4. eliminate all existentials ! (discussedlater)
5.!move universals to the front ! using ∀x[α]∧βß ∀x[α∧
β]+ + + 6.!distribute ∨over ∧
7.!collect terms
where z is a new
where βdoes not use x
Get universally quantified conjunction of disjunction of literals
! then drop the quantifiers…
KR & R! © Brachman & Levesque 2005
Resolution
First-order resolution
Main idea:
! a literal (with variables) stands for all its instances; will allow all such inferences
So given:
! [P(x,a),¬Q(x)]and[¬P(b,y),¬R(b,f(y))], ! want to infer: [¬Q(b), ¬R(b,f(a))]
! since ! [P(x,a), ¬Q(x)] has [P(b,a), ¬Q(b)] and
! ! [¬P(b,y),¬R(b,f(y ))] has [¬P(b,a), ¬R(b,f(a))]
Resolution:
! Given clauses: {l1} ∪ C1 and {¬ l2} ∪ C2
! Rename variables, so that distinct in two clauses.
! Foranyθsuchthatlθ=lθ,caninfer(C ∪C)θ.
+ We say that l1 unifies with l2 and that θ is a unifier of the two literals
Resolution derivation: as before
still ignoring =
1 2
1 e2xample below
Theorem: S |⎯ [] iff S |= []
! ! ! iff S is unsatisfiable
KR & R! © Brachman & Levesque 2005
Resolution
Example 3
KB:
! ∀x GradStudent(x) ⊃ Student(x) ! ∀x Student(x) ⊃ HardWorker(x) ! GradStudent(sue)
Q:! HardWorker(sue) [¬Student(x), HardWorker(x)]
x/sue
[¬GradStudent(x), Student(x)] x/sue
[GradStudent(sue)]
Can label each step with the unifier
[¬HardWorker(sue)]
[¬Student(sue)] [¬GradStudent(sue)]
[]
KR & R! © Brachman & Levesque 2005
Resolution
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
[¬On(x,y), ¬Green(x), Green(y)]
[On(b,c)]
{x/b, y/c} [¬Green(b), Green(c)]
[¬Green(c)]
[¬Green(b)]
Note: Need to use On(x,y) twice, for 2 cases
{x/a, y/b} [¬Green(a), Green(b)]
[Green(b)] []
[On(a,b)]
[Green(a)]
KR & R! © Brachman & Levesque 2005
Resolution
Arithmetic
KB:
Q:!
! ! !
! ! !
Plus(zero,x,x)
Plus(x,y,z) ⊃ Plus(succ(x),y,succ(z))
∃u Plus(2,3,u)
where for readability, we use
! 0 forzero,
! 3 for succ(succ(succ(zero))) etc.
[¬Plus(x,y,z), Plus(succ(x),y,succ(z))] [Plus(0,x,x)]
Can find the answer in the derivation
u/succ(succ(3)) i.e u/5
Can derive Plus(2,3,5)
[¬Plus(2,3,u)]
x/1, y/3, u/succ(v), z/v
[¬Plus(1,3,v)]
x/0, y/3, v/succ(w), z/w
[¬Plus(0,3,w)] x/3, w/3
[] Rename variables
to keep them distinct
KR & R! © Brachman & Levesque 2005
Resolution
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)]
! whereAisanewpredicatesymbolcalledtheanswerpredicate • instead of deriving [], derive any clause containing just the
answer predicate
• canalwaysconvertaderivationof[]
Example KB:
+ {Student(john), Student(jane), Happy(john)}
Q:! ∃x[Student(x) ∧ Happy(x)]
Student(jane)
⇓
[¬Student(x), ¬Happy(x), A(x)] {x/john}
Happy(john)
Student(john) [¬Student(john), A(john)]
[A(john)] An answer is: John
KR & R! © Brachman & Levesque 2005
Resolution
Disjunctive answers
Example KB:
Q:!
+
+
{Student(john), Student(jane), ! ! [Happy(john) ∨ Happy(jane)]}
∃x[Student(x) ∧ Happy(x)] [¬Student(x), ¬Happy(x), A(x)]
Student(jane)
{x/jane}
[¬Happy(jane), A(jane)] [Happy(john), Happy(jane)]
Student(john) {x/john}
[¬Happy(john), A(john)]
⇓
[Happy(john), A(jane)]
[A(jane), A(john)]
Note:
• can have variables in answer
• need to watch for Skolem symbols…
(next)
An answer is: either Jane or John
KR & R! © Brachman & Levesque 2005
Resolution
Skolemization
So far, converting wff to CNF ignored existentials ! ! e.g. ∃x∀y∃zP(x,y,z)
Idea: names for individuals claimed to exist, called Skolem constant and function symbols
there exists an x, call it a
for each y, there is a z, call it f(y) ! ! get ∀yP(a,y,f(y))
In general:
+ ∀x1(…∀x2(…∀xn(…∃y[… y …] …)…)…)
is replaced by
+ ∀x1(…∀x2(…∀xn( … [… f(x1,x2,…,xn) …] …)…)…)
! wherefisanewfunctionsymbolthat appears nowhere else
Skolemization does not preserve equivalence ! e.g. |≠ ∃xP(x) ≡ P(a)
But it does preserve satisfiability
! α is satisfiable iff α′ is satisfiable
where α′ is the result of skolemization Sufficient for resolution!
KR & R! © Brachman & Levesque 2005
Resolution
Variable dependence
Show that ∃x∀yR(x,y) |= ∀y∃xR(x,y)
! show {∃x∀yR(x,y), ¬∀y∃xR(x,y)} unsatisfiable
! ∃x∀yR(x,y) ß ∀yR(a,y)
! ¬∀y∃xR(x,y) ß ∃y∀x¬R(x,y) ß ∀x¬R(x,b) ! then {[R(a,y)], [¬ R(x,b)]} |⎯ [] with {x/a, y/b}.
Show that ∀y∃xR(x,y) |≠ ∃x∀yR(x,y)
! show {∀y∃xR(x,y), ¬∃x∀yR(x,y)} satisfiable
+ ∀y∃xR(x,y) ß ∀yR(f(y),y)
! ¬∃x∀yR(x,y) ß ∀x∃y¬R(x,y) ß ∀x¬R(x,g(x)) ! then get {[R(f(y),y)], [¬ R(x,g(x)]}
+ where the two literals do not unify +
Note:
! important to get dependence of variables correct
+ R(f(y),y) vs. R(a,y) in the above
first argument depends on second one here
KR & R! © Brachman & Levesque 2005
Resolution
A problem
KB:! LessThan(succ(x),y) ⊃ LessThan(x,y) Q:! LessThan(zero,zero)
Should fail since KB |≠ Q [LessThan(x,y), ¬LessThan(succ(x),y)]
[¬LessThan(0,0)] x/0, y/0
[¬LessThan(1,0)] x/1, y/0
[¬LessThan(2,0)] x/2, y/0
…
Infinite branch of resolvents
! cannot use a simple depth-first procedure to search for []
…
KR & R! © Brachman & Levesque 2005
Resolution
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
Also true for Horn clauses
(later)
!
some branch will contain [], for unsat clauses
… infinite
branches
…
…
[]
So breadth-first search guaranteed to find [] ! search may not terminate on satisfiable clauses
KR & R! © Brachman & Levesque 2005
Resolution
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), …
! unifiedby
! θ1 = {x/b, y/g(b), z/a, w/b}
+ gives P(g(b),f(b),a)
! andby
! θ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!
KR & R! © Brachman & Levesque 2005
Resolution
Most general unifiers
θ is a most general unifier of literals l1 and l2 iff
1.!
2.! ! !!
θ unifies l1 and l2
for any other unifier θ′, there is a another ! substitution θ* such that θ′ = θθ* 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.!!
2.!! !
3.!!
!
4.!! 5.!!
Start with θ = {}.
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)}
Find a variable v ∈DS, and a term t ∈DS
not containing v. If not, fail. θ= θ{v/t}
Go to 2
Note: there is a better linear algorithm
KR & R! © Brachman & Levesque 2005
Resolution
Herbrand Theorem
Some 1st-order cases can be handled by converting them to a propositional form
Given a set of clauses S
• theHerbranduniverseofSisthesetofalltermsformed 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))), …}
• theHerbrandbaseofSis
+ {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
KR & R! © Brachman & Levesque 2005
Resolution
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
! Evenifwecouldalwaysfindaderivationimmediately, 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 by most people to be unsolvable in polynomial time
KR & R! © Brachman & Levesque 2005
Resolution
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
! proceduralrepresentations(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
! needtobecarefultopreservecompleteness
! ATP: automated theorem proving
! area that studies strategies for proving difficult theorems
! main application: mathematics, but relevance also to KR
KR & R! © Brachman & Levesque 2005
Resolution
Strategies
1.!
Clause elimination • pureclause
! 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 • subsumedclause
! 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
Ordering strategies
! many possible ways to order search, but best and simplest is
• unitpreference
! prefer to resolve unit clauses first
! Why? Given unit clause and another clause, resolvent is a smaller one ß []
2.!
KR & R! © Brachman & Levesque 2005
Resolution
Strategies 2
3.!
!
4.!
!
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)
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 []
KR & R! © Brachman & Levesque 2005
Resolution
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′…)} ∪ C2 ! where tθ= t′θ
! infer {P(… s …)}θ ∪ C1θ ∪ C2θ.!
! collapses many resolution steps into one
6.!
!
! see also: theory resolution (later)
[father(john)=bill] [Married(father(x),mother(x))] [Married(bill,mother(john))]
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 []
KR & R! © Brachman & Levesque 2005
Resolution
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
KR & R! © Brachman & Levesque 2005
Resolution