Chapter 9
Inference in First-Order Logic  

9.1 PROPOSITIONAL VS. FIRST-ORDER INFERENCE

 

• ground term - a term without variables
• substitution binding

  For the KB with assertions:

  • King(John)
  • Greedy(John)
  • King(Richard)
  • Greedy(Richard)

  "x King(x) Ù Greedy(x) Þ Evil(x) returns the binding {x/John, x/Richard}

Universal instantiation

"x King(x)
_________________________________
SUBST({x/John, x/Richard}, "x King(x)

yields:

King(John)
King(Richard)
 

"x King(x) Ù Greedy(x) Þ Evil(x)
__________________________________________________
SUBST({x/John, x/Richard}, "x King(x) Ù Greedy(x) Þ Evil(x) )

yields:

King(John) Ù Greedy(John) Þ Evil(John)
King(Richard) Ù Greedy(Richard) Þ Evil(Richard)

These sentences can be added to KB

 

For the KB with assertions: Brother(John, Richard) Brother(Richard, John) Brother(Harry,John) What are the substitutions for universal instantiation? "x Brother(John, x) Þ King(x) "x Brother(x, John) Þ King(x) "x,y Brother(x, y) Þ King(x)

Existential Instantiation

• For the KB with assertions:
  • King(John)
  • Brother(John, Richard)
  • King(Richard)
  • Brother(Richard, John)

  Queries to the KB

  $x King(x) Ù Brother(x, Richard) returns the binding {x/John}
  $x,y King(x) Ù Brother(x, y) returns the bindings
                                              {x/John, y/Richard}{x/Richard, y/John}
   

Existential instantiation

For the KB with assertions:

• King(John)
• Brother(John, Richard)
• King(Richard)
• Brother(Richard, John)
• $x King(x) Ù Brother(x, Richard)

$x King(x) Ù Brother(x, Richard)
__________________________________________________
SUBST({x/J}, "x King(x) Ù Brother(x, Richard) )

yields:

King(J) Ù Brother(J, Richard)

replacing:

$x King(x) Ù Brother(x, Richard)

in KB which now appears as:

• King(John)
• Brother(John, Richard)
• King(Richard)
• Brother(Richard, John)
• King(J) Ù Brother(J, Richard)

 

For the KB with assertions: King(John) Brother(John, Richard) King(Richard) Brother(Richard, John) What is the result of existential instantiation? $x King(x) Ù Brother(x, John) $x,y King(x) Ù Brother(x, y)

Benefit

Translates quantified KB to propositional KB, can use any complete propositional inferencing algorithms.

Problem

Any KB with function can have infinite number of ground term substitutions. Example: Father(Father(Father(......

 

For the KB: King(John) Brother(Richard, John) Smelly(wumpus) "x King(x) Þ Evil(x) Which are the result of propositionalization of "x King(x) Þ Evil(x)? King(John) Þ Evil(John) King(Richard) Þ Evil(Richard) King(wumpus) Þ Evil(wumpus) King(wumpus) Þ Smelly(wumpus) King(John) Þ Smelly(John) Which are entailed by KB?

9.2 UNIFICATION AND LIFTING

Unification

• Finding substitutions that make different logical sentences look identical.
• Converting KB from FOL by propositionalization is inefficient and may not terminate if sentence to prove is not entailed.
• Unification, combined with General Modus Ponens, forms FOL inference method.
• Can get inference immediately if a substitution exists that makes premise of the implication identical to sentences already in KB.

KB

"x King(x) Ù Greedy(x) Þ Evil(x)
King(John)
Greedy(John)

Substitution

"x King(x) Ù Greedy(x) Þ Evil(x)
__________________________________________________
SUBST({x/John}, "x King(x) Ù Greedy(x) Þ Evil(x) )

yields:

King(John) Ù Greedy(John) Þ Evil(John)

If, instead the KB was:

"x King(x) Ù Greedy(x) Þ Evil(x)
King(John)
"y Greedy(y)

Requires two substitutions:

S1

"y Greedy(y)
__________________________________________________
SUBST({y/John}, "y Greedy(y))

S2

"x King(x) Ù Greedy(x) Þ Evil(x)
__________________________________________________
SUBST({x/John}, "x King(x) Ù Greedy(John) Þ Evil(x) )

yields:

King(John) Ù Greedy(John) Þ Evil(John)

 

Inferencing by substitution

King(John) Ù Greedy(John) Þ Evil(John)

can now infer:

Evil(John)

Unify(p,q) = q where Subst(q,p) = Subst(q,q)

1. Unify(Knows(John,x),Knows(John,Jane)) = { x/Jane}
2. Unify(Knows(John,x),Knows(y,Mother(y))) = { y/John, x/Mother(John)}
3. Unify(Knows(John,x),Knows(x,Jane)) = fail
   because x ≠ John and Jane at same time.

   Can rename Knows(x, Jane) to Knows(y,Jane)

4. Unify(Knows(John,x),Knows(y,Jane)) = { y/John, x/Jane}

KB King(John) Brother(John, Richard) King(Richard) Brother(Richard, John) What is the result of: Unify(King(Richard), King(x)) Unify(King(x), King(y)) Unify(King(Richard) Þ Brother(Richard, John), King(x) Þ Brother(x, John)) Unify(King(x) Þ Brother(Richard, x), King(y) Þ Brother(y, John))  Unify(King(x) Þ Brother(Richard, x), King(x) Þ Brother(x, John))

 

Most General Unifier (MGU)

KB

• King(John)
• King(Richard)

Unify( King(x), King(y)) could be:

{ y/John, x/John} or { y/Richard, x/Richard}

either obviously not the most general.

MGU is a variable rather than a constant:

{ y/z, x/z}

yielding:

King(z)

What is the MGU of: Unify(King(x) Þ Brother(x,Richard), King(y) Þ Brother(y, Richard)) Unify(King(x) Þ Brother(x,y), King(a) Þ Brother(a,b))

Says that given sentences p^'_i are true, p_i are true, and a substitution q exists where  p^'_iq=p_iq then qq is true.

Recall that (Øp₁ÚØp₂Úq)  º p₁Ùp₂Þq

p Þ q, p
_______
   q

Insight is that given sentences p^'_iq are true and p^'_iq=p_iq

9.3 FORWARD CHAINING

First-order definite clauses

First-order definite clauses can contain variables; assumed universally quantified. Suitable for Generalized Modus Ponens.

Examples:

• King(x) Þ Brother(Richard, x)
• King(John)
• King(x)

Datalog KB (e.g. above) comprised of:

1. first-order definite clauses
2. variables
3. NO function symbols

 

Discussion

Forward-chaining attempts to unify a query with KB.

• Start with KB as first-order definite clauses (one positive literal forms head (conclusion) and negated literals form body (premise)).
• Repeat until unification or no new conclusions added to KB.
  • for all sentences in KB (add at most one new conclusion each iteration)
    • Standardize apart by uniquely renaming variables in sentence r.
    • Apply generalized modus ponens to each sentence with implication premise satisfied (all p_i are known to be true) to produce a conclusion.
    • If new conclusion reached
      • Add the conclusion (an atomic sentence) to new conclusions.
      • If unify conclusion with query return unification
  • Add new conclusions to KB
• Unification failed, return false

   

Is West a Criminal?
Criminal(West)

The known facts.

From satisfied implications, add conclusions to premises.

The proof: Criminal(West)

The diagram at right illustrates the forward chaining performed to prove all possible: Valuable( x ) using the clause at the top of the diagram. There are two bindings that satisfy the clause. For the KB of: Horse(Prancer). Horse(Thunder). Horse(Comet). Horse(Dasher). Fast(Thunder). Fast(Prancer). Parent(Dasher,Comet). Parent(Prancer,Comet). Parent(Thunder,Dasher). "x,y Horse(x) Ù Parent(y,x) Ù Fast(y) Þ Valuable(x) The parent of a fast horse is valuable. Prove: Valuable(Comet) Valuable(Dasher) Valuable(Prancer)

9.4 BACKWARD CHAINING

    Algorithm

1. Initially goals stack contains the one query goal.
2. If no goals remain return answer (substitutions necessary to unify query goal).
3. Use an existing substitution to produce q' from first remaining goal, if none exists q' is just the goal without substitution.
4. For each clause in KB whose head (positive literal or conclusion) unifies with goal (under a substitution). A fact is a clause with only a head.
   • Premise (p₁,...,p_n) of each clause added to goal stack as a subgoal [p₁,...,p_n|Rest(goals)]
   • Compose(new substitution with current substitutions).
5. Finished when no new subgoals added, return composed substitutions. Composed substitutions avoid conflicts between substitutions (e.g. q₁={x/Nono} and q₂={x/West})

SUBST(COMPOSE(q₁, q₂),p) = SUBST(q₂, SUBST(q₁,p))

Example clauses

Is West a Criminal?
Criminal(West)

Goal: Criminal(West)

Subgoals: each conjunctive

 

Unify: Missile(y) {y/M₁)

Backchaining: Valuable( z )

Binds z to all objects (Dasher, Comet) satisfying:

"x,y Horse(x) Ù Parent(y,x) Ù Fast(y) Þ Valuable(x)

Backchaining: Valuable( z )

Binds z to all objects (Dasher, Comet, Prancer) satisfying:

• "x,y Horse(x) Ù Parent(y,x) Ù Fast(y) Þ Valuable(x)
• "w Winner(w)  Þ Fast(w)
• Winner(Prancer)
• Winner(Dasher)
• Horse(Prancer).
• Horse(Thunder).
• Horse(Comet).
• Horse(Dasher).
• Fast(Thunder).
• Fast(Prancer).
• Parent(Dasher,Comet).
• Parent(Prancer,Comet).
• Parent(Thunder,Dasher).

Note that Prancer required backchain to prove conclusion Fast(Prancer) by premise Winner(w). That conclusion again proved Valuable(Comet)

Also that could not prove the conclusion Fast(Thunder) by premise Winner(w) (there is no Winner(Thunder)).

Prolog program to prove criminal(west)

weapon(X) :- missile(X). criminal(X) :- american(X), weapon(Y), sells(X,Y,Z),hostile(Z). sells(west,X,nono) :- missile(X),owns(nono,X). hostile(X) :- enemy(X,Y). enemy(nono,america).american(west). owns(nono,m1). missile(m1).

?- criminal(west). Yes ?- weapon(X).                                      {X/m1} X = m1 ;   ?- sells(west,X,nono).                            {X/m1} X = m1 ; ?- hostile(X). X = nono                                              {X/nono}

 

Prolog family program

% father(P,C) v mother(P,C) => parent(P,C) parent(P,C) :- father(P,C); mother(P,C).                                     % parent(P,S1) ^ parent(P,S2) ^ S1 != S2 =>siblings(S1,S2) siblings(S1,S2) :- parent(P,S1), parent(P,S2), S1\=S2. cousins(X,Y) :- parent(P1,X),parent(P2,Y),siblings(P1,P2).

father(daddieWumpus,wumpusJr). mother(mommieWumpus,wumpusJr). mother(mommieWumpus,girlieWumpus). father(wumpusJr,wumpusJrJr). mother(girlieWumpus,girliegirlieWumpus).

?- parent(wumpusJr,wumpusJrJr ). Yes ?- parent(wumpusJr,X). X = wumpusJrJr ; ?- father(X,Y). X = daddieWumpus Y = wumpusJr ; X = wumpusJr Y = wumpusJrJr ; ?- cousins(X,Y). X = wumpusJrJr Y = girliegirlieWumpus ; X = girliegirlieWumpus Y = wumpusJrJr ;

Prolog basic syntax

• Objects - lowercase. john, etc.
• Rules - lowercase names. Example: loves(john,X). Terminated by a period.
• Variables - uppercase names. loves(X,mary).

Prolog basic operations

• and                   ,
• or                     ;
• implication        conclusion :- premise.
• not                  not
• assignment       is
• fail                   return false
• !                      fence, don't backtrack over.

Backtracking - Prolog produces multiple substitution bindings to variables through backtracking. The following illustrates that all substitutions that unify the clause child(A, B) :- a(A, B) are produced.

a(a,b).                              a(a,c). %           /        |       \                       /             \       a(b,d).   a(b,e).   a(b,f).       a(c,g).             a(c,h). %                                |               |                  /      \                                 a(f,q).      a(g,i).       a(h,j).    a(h,k).   child(A,B) :- a(A,B).                       % Child relation gc1(A,B) :- a(A,C), a(C,B).              % Grandchild relation gc2(A,B) :- a(A,C), !, a(C,B). gc3(A,B) :- a(A,C), a(C,B), !.

?- child(X,Y).      % Backtracking re-instantiates a(A,B) X = a      X = a     X = b    X = b    X = b   X = f     X = c    X = c Y = b ;    Y = c ;   Y = d ;  Y = e ;  Y = f ;  Y = q ;  Y = g ;  Y = h ; X = g      X = h     X = h Y = i ;     Y = j ;    Y = k ; ?- gc1(X,Y).         % Backtracking re-instantiates a(A,C), a(C,B); binding succeeds when grandchild     X = a    X = a    X = a    X = a    X = a    X = b    X = c    X = c  X = c     Y = d ;  Y = e ;  Y = f ;   Y = g ;  Y = h ;  Y = q ; Y = i ;   Y = j ; Y = k ;  ?- gc2(X,Y).         % Fence prevents backtracking to re-instantiate a(A,C); succeeds when grandchild     X = a    X = a    X = a     Y = d ;  Y = e ;  Y = f ;  ?- gc3(X,Y).         % Fence prevents backtracking to re-instantiate a(A,C), a(C,B); succeeds when grandchild     X = a     Y = d ;

 

DFS is performed to find the path to k on the facts a(X,Y) which form a tree with a at the root. The path is (a,c,h,k), the k results from satisfying the goal(State), dfs(State) produced the remainder in the order bound.

Note that successor(State,Successor) binds Successor when State matches (e.g. successor(b,e)). On failure (e.g. successor(e,Successor)) backtracking occurs and any bindings at that level are lost.

The simplest view of backtracking results is it produces only bindings that lead to a unification.

Prolog dfs program

dfs(State) :- goal(State). dfs(State) :- successor(State, Successor), dfs(Successor). successor(State, Successor) :- a(State,Successor).

a(a,b).                              a(a,c). %           /        |       \                       /             \       a(b,d).   a(b,e).   a(b,f).       a(c,g).             a(c,h). %                                |               |                  /      \                                 a(f,q).      a(g,i).       a(h,j).    a(h,k). goal(k).

dfs(X).   X = k ;   X = a ;   X = c ;   X = h ;

 

 

Convert to CNF "x Animal(x)  Þ Loves(Jack, x) "x [$y Animal(y) Ù Kills(x,y) Þ "z ØLoves(z,x)] "x ["y Animal(y) Ù Kills(x,y) Þ "z ØLoves(z,x)]

 

Resolution Proof that Curiosity killed the Cat

1. "x ["y Animal(y) Þ Loves(x,y)] Þ [$y Loves(y,x)]
2. "x [$y Animal(y) Ù Kills(x,y)] Þ ["z ØLoves(z,x)]
3. "x Animal(x)  Þ Loves(Jack, x)
4. Kills(Jack,Tuna) Ú Kills(Curiosity,Tuna)
5. Cat(Tuna)
6. "x Cat(x)  Þ Animal(x)
7. ØKills(Curiosity,Tuna)

Converting to CNF

A1. Animal(F(x)) Ú Loves(G(x),x)
A2. ØLoves(x,F(x)) Ú Loves(G(x),x)
B.   ØAnimal(y) Ú ØKills(x,y) Ú ØLoves(z,x)
C.   ØAnimal(x) Ú Loves(Jack, x)
D.   Kills(Jack,Tuna) Ú Kills(Curiosity,Tuna)
E.   Cat(Tuna)
F.   ØCat(x)  Ú Animal(x)
G.  ØKills(Curiosity,Tuna)

Prove:  Criminal(West)

Prove using resolution: Above(B, Table) ØOn(u, v) Ú Above(u, v) ØAbove(x, y) Ú ØAbove(y, z) Ú Above(x, z) On(B, A) On(A, Table)