一階邏輯的推論法則有很多種，但是其中最簡單且優美的莫過於羅氏 (Robinson) 推論法則，該方法只用了一條推論法則 Resolution，然後利用矛盾法進行推論。
Chapter 9: Inference in first order logic
SUBST(b, φ) :
the result of applying the substition b to the sentence φ.
b is a binding list
example : SUBST({x/Sam, y/Pam}, Likes(x,y)) = Likes(Sam, Pam)
Inference rule :
1. Universal elimination :
$v φ => SUBST({v, g}, φ) where g is any ground term.
2. Existential elimination :
#v φ => SUBST({v, k}, φ)
where k is a constant symbol that does not appear elsewhere.
3. Existential Introduction :
φ => #v SUBST({g/v}, φ) where g is a ground term, v is a variable.
Generalized Modus Ponens
if SUBST(theta, pi')=SUBST(theta, pi) then
p1',p2', ...,pn', (p1&p2&...&pn=>q) => SUBST(theta, q)
Horn Sentence
Unification
UNIFY(p, q) = theta if SUBST(theta, p)=SUBST(theta, q)
where the UNIFY return the Most General Unifier (MGU)
example:
UNIFY(Knows(John, x), Knows(y, z))
may have {y/John, x/z}, {y/John, x/John, z/John}...
but {y/John, x/z} use the least commitment
Forward Chaining Algorithm ( is a data-driven (data-directed) procedure)
Renaming : Likes(x, IceCream) = Likes(y, IceCream)
Composition : COMPOSE(theta1, theta2)
SUBST(COMPOSE(theta1, theta2), p) = SUBST(theta2, SUBST(theta1, p))
procedure FORWARD-CHAIN(KB, p)
if there is a sentence in KB that is a renaming of p then
return
Add p to KB // 新加入一條 fact, 盡可能的去觸發所有可能的 unification.
for each (p1&...&pn=>q) in KB
such that for some i, UNIFY(pi, p)= theta succeeds do
FIND-AND-INFER(KB, [p1,...,Pi-1,Pi+1,...Pn], q, theta)
end
procedure FIND-AND-INFER(KB, premoses, concolusion, theta)
if premise = [] then
// 本規則完全 unify 成功, 把 conclusion 也加入, 並看能否進一步觸發其它規則.
FORWARD-CHAIN(KB, SUBST(theta, conclusion))
else for each p' in KB such that UNIFY(p', SUBST(theta, FIRST(premises))) = theta2 do
// 把可以 unify 的規則一直 unify 到無法 unify 為止.
FIND-AND-INFER(KB, REST(premise), conclusion, COMPOSE(theta, theta2))
end
function BACK-CHAIN(KB, q) returns a set of substitutions
BACK-CHAIN-LIST(KB, [q], {})
function BACK-CHAIN-LIST(KB, qlist, theta) returns a set of substitutions
input : KB, a knowledge base
qlist, a list of conjuncts forming a query (theta already applied)
theta, the current substitution
local variables : answers, a set of substitutions, initially empty
if qlist is empty then
return {theta}
q = FIRST(qlist)
for each qi' in KB such that theta i = UNIFY(qi, qi') succeeds do
Add COMPOSE(theta, theta i) to answer
end
for each sentence (p1&...&pn=>qi') in KB such that theta i = UNIFY(q, q') succeeds do
answers = BACK-CHAIN-LIST(KB, SUBST(theta i, [p1,...,pn]), COMPOSE(theta, theta i)) ∪ answers
end
return the union of BACK-CHAIN-LIST(KB, REST(qlist), theta) for each theta in answers.
KB :
American(x) & Weapon(y) & Nation(z) & Hostile(z) & Sells(x, z, y) => Criminal(x)
Owns(Nono, x) & Missile(x) => Sells( West, Nono, x)
Missile(x) => Weapon(x)
Enemy(x, America ) => Hostile(x)
FACTS :
American(West)
Nation(Nono)
Enemy(Nono, America)
Owns(Nono, M1)
Missile(M1)
Forward chaining example
{American(West)} & Weapon(y) & Nation(z) & Hostile(z) & Sells(West, z, y) => Criminal(West)
{Nation(Nono)} & American(x) & Weapon(y) & Hostile(z) & Sells(x, z, y) => Criminal(x)
{American(West) & Nation(Nono)} & Weapon(y) & Hostile(Nono) & Sells(x, z, y) => Criminal(West)
{Enemy(Nono, America)} ... => Hostile(Nono)
{American(West) & Nation(Nono) & Hostile(Nono)} & Weapon(y) & Sells(West, Nono, y) => Criminal(West)
{Owns(Nono, M1) } & Missile(M1) => Sells( West, Nono, M1)
{Owns(Nono, M1) , Missile(M1) } ... => Sells(West, Nono, M1)
{American(West) & Nation(Nono) & Hostile(Nono) & Sells(West, Nono, M1) } & Weapon(y) => Criminal(West)
{ Missile(M1) } ...=> Weapon(M1)
{American(West) & Nation(Nono) & Hostile(Nono) & Sells(West, Nono, M1) & Weapon(M1)} ...=> Criminal(West)
question sentence found.
Backward chaining example
? Criminal(West):?American(West)&?Weapon(y)&?Nation(z)&?Hostile(z)&?Sells(West, z, y): yes
? American(West) : yes-^ ^ ^ ^ ^
? Weapon(y) : ? Missile(y) : Missile(M1) {y/M1} | | |
? Nation(z) : Nation(Nono) {z/Nono}-------------+ | |
? Hostile(Nono) : yes-----------------------------------------+ |
? Sell(West, Nono, M1) : yes -------------------------------------------+
Forward chaining and Backward chaining is not complete
Proof :
In Case Analysis
KB :
$x P(x) => Q(x)
$x -P(x)=> R(x)
$x Q(x) => S(x)
$x R(x) => S(x)
---------------
KB ╞ $x S(x) but KB !╞ $x S(x) in Forward chaining and Backward chaining.
Complete : if KB╞φ then KB ├ φ by Resolution Procedure
Resolution in and/or form
(a|b) & (-b|c) => a|c
Resolution in implication form
(-a=>b & b=>c) => -a=>c
Generalized Resolution in and/or form
[p] = [p1|...pj...|pm]
[q] = [q1|...qk...|qn]
[p] &[q] => SUBST(theta, [p]-pj, [q]-qk)
where UNIFY(pj, -qk) = theta
Generalized Resolution in implication form
[p] = [p1&...pj...&pn1]
[r] = [r1|........|rn2]
[s] = [s1&........&sn3]
[q] = [q1|...qk...|qn4]
(([p] => [r]) & ([s] => [q])) => SUBST(theta, (([p]-pj)&[s])=>([r]|([q]-qk))))
(where UNIFY(pj, -qk) = theta )
Canonical form for resolution :
Conjunctive normal form (CNF)
-P(w)|Q(w)
P(x)|R(x)
-Q(y)|S(y)
-R(z)|S(z)
Implicative Normal Form (INF)
P(w)=>Q(w)
True=>P(x)|R(x)
Q(y)=>S(y)
R(z)=>S(z)
P(w)=>Q(w) Q(y)=>S(y)
\ {y/w} /
P(w)=>S(w) True=>P(x)|R(x)
\ {w/x} /
True=>S(x)|R(x) R(z)=>S(z)
\ {x/A,z/A} /
True=>S(A) S(A)=>False
\ /
True=>False
-P(w)|Q(w) -Q(y)|S(y)
\ {y/w} /
-P(w)|S(w) P(x)|R(x)
\ {w/x} /
S(x)|R(x) -R(z)|S(z)
\ {x/A,z/A} /
S(A) -S(A)
\ /
FALSE
Conversion to Normal Form
Eliminate implication
(p=>q) ├ (-p|q)
Move - inwards
-(p|q) ├ (-p&-q)
-(p&q) ├ (-p|-q)
-($x,p)├ (#x -p)
--p ├ p
Standardize variables
rename variable in different scope with different name.
Move quantifiers left
p|$x q ├ $x p|q
Skolemize : removing # by elimination.
$x Person(x) => #y Heart(y)&Has(x, y)
->$x Person(x) => Heart(F(x))&Has(x, F(x))
Distribute & over | :
(a&b)|c -> (a|c)&(b|c)
Flatten nested conjunctions and disjunctions :
(a|b)|c -> (a|b|c)
Convert disjunctions to implications
(-a|-b|c|d) -> (a&b=>c|d)
Example Proof :
In implication normal form :
Axiom :
#x Dog(x)&Own(Jack, x)
$x(#y Dog(y)&Own(x, y))=>AnimalLover(x))
$x(AnimalLover(x)=>($y -Animal(y)=>-Kill(x,y)))
$x(Cat(x)=>Animal(x))
Dog(D)
Own(Jack, D)
Cat(Tuna)
Kills(jack, Tuna)|Kills(Curiosity, Tuna)
In implication form:
$x(#y Dog(y)&Own(x, y))=>AnimalLover(x))
Dog(F1[x])
$x$y(AnimalLover(x)=>(Animal(y)=>-Kill(x,y)))
$x(Cat(x)=>Animal(x))
Dog(D)
Own(Jack, D)
Cat(Tuna)
Kills(Jack, Tuna)|Kills(Curiosity, Tuna)
Dog(D) Dog(y)&Own(x, y)=>AnimalLover(x)
\ / {y/D}
Own(x, D)=>AnimalLover(x) Own(Jack, D)
{x/Jack} \ /
AnimalLover(x)=>(-Animal(y)=>-Kill(x, y)) AnimalLover(Jack)
\ /
Cat(Tuna) Cat(x)=>Animal(x) Animal(y)=>-Kill(Jack, y)
\ / /
Animal(Tuna) /
\ /
-Kill(Jack, Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna)
\ /
Kill(Curiosity, Tuna) -Kill(Curiosity, Tuna)
\ /
False
In conjunction normal form :
-Dog(y)|-Own(x, y)|AnimalLover(x)
Dog(F1[x])
-AnimalLover(x)|-Animal(y)|Kill(x,y)
-Cat(x)|Animal(x)
Dog(D)
Own(Jack, D)
Cat(Tuna)
Kills(Jack, Tuna)|Kills(Curiosity, Tuna)
Dog(D) -Dog(y)|-Own(x, y)|AnimalLover(x)
\ / {y/D}
-Own(x, D)|AnimalLover(x) Own(Jack, D)
{x/Jack} \ /
-AnimalLover(x)|-Animal(y)|Kill(x, y) AnimalLover(Jack)
\ /
Cat(Tuna) -Cat(x)|Animal(x) -Animal(y)|Kill(Jack, y)
\ / /
Animal(Tuna) /
\ /
-Kill(Jack, Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna)
\ /
Kill(Curiosity, Tuna) -Kill(Curiosity, Tuna)
\ /
False
Dealing with equality
A=B & P(A) cannot unify with P(B), it’s unreasonable.
Method 1 : Axiomize equality
$x x=x
$x,y x=y => y=x
$x,y,z x=y & y=z => x=z
$x,y x=y => (P1(x)<=>P1(y))
..
..
$w,x,y,z w=y&x=z => (F(w,x)=F(y,z))
..
..
Method 2 : Demodulation
UNIFY(x,z)= theta & x=y, (.. z .. ) => (.. SUBST(theta, y) ..)
Resolution strategy
Unit preference (Wos 1964): 短者優先
Set of support (Wos 1965):
1. identify set of support
2. combine(x,y) x in set of support, y in KB
Input resolution :
combine(x,y) x is input sentence, y in KB
In Horn clause , input resolution is complete.
Linear resolution (Loveland 1968):
if P=>..=>Q then Q, Q
then Unify(P,z), Unify(Q,z) should be done together.
Subsumption :
eliminates all sentences that are subsumed by an existing sentence in the KB.
Example : if P(x) in KB then P(A) should be deleted from axiom.
Post preview:
Close preview