# 訊息

## English

``````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
end
for each sentence (p1&...&pn=>qi') in KB such that theta i = UNIFY(q, q') succeeds do
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.```
```