COSC 3402 Artificial Intelligence

<<< Resolution

Predicate Logic (Review)

PL = < L_PL, |--_PL >

A predicate logic language:

• Individual variables: x,y,z,x₁,y₁,z₁,...
• Constant symbols: c₁,...,c_k (e.g. 0,1)
• Function symbols: f₁,...,f_m (e.g. +,*,temp(day),...)
• Predicate symbols (relations): p₁,...,p_n (e.g. =,>,prime(x),...)
• Logical Connectives: ¬, v, ^, -->, =
• Quantifiers: forall, exists

Definition: The set TERM of terms is the smallest set such that:

1. Every variable and every constant is in TERM
2. If f is a function symbol of n arguments and if t₁,...,t_n E TERM, then f(t₁,...,t_n) E TERM

Ex. 1,0,x,y E TERM (by 1)
    1+1, 0*1 E TERM (by 2)
    temp((1+1)*(0*1)) E TERM (by 2)
    1++ /E TERM (1++ is +(+,1) but + is neither a variable nor constant)

Atomic Formulas: P(t₁,...,t_k) - a predicate symbol P applied to the terms. e.g. =(1,0), 1 < 2, prime(12), ...

Formulas: The smallest set FOR such that:

1. Every atmoic formula is a formula
2. if α, β E FOR then ¬α, α V β, α ^ β, α --> β, α = β E FOR
3. If α E FOR and if x is a variable, then:
   (forallx α) and (existsx α) are in FOR

Ex: x < 2 + y E FOR (by 1)
    prime(x) E FOR (by 1)
    ¬prime(x) v (x < 2 + y) E FOR (by 2)
    forallx(¬prime(x) v (x < 2 + y)) E FOR (by 3)
    ¬forallx(¬prime(x) v (x < 2 + y)) E FOR (by 2)

Example: Block World
A block consists of 3 objects:
     (a robot R, a number of blocks (A,B,...) and an environment)
     
      B
     |A| |R| | |C| | |
      0 1 2 3 4 5 6 7     
      
Design a predicate logic language to represent this world.

Constant symbols: R, A, B, C, 0, 1, 2, ..., 7
Function symbols: energy(t)
Predicate symbols: on(_,_), block(_), close(_,_), clear(_).

KB = {block(A),block(B),block(C),
      on(A,0), on(B,A), on(R,2), on(C,5),
      clear(B), clear(C), clear(1), clear(3), clear(4), clear(6), clear(7),
      forallxyz(on(y,x) ^ on(z,y) --> on(z,x))}
      
/* Queries */
KB |-?- on(B,A)    yes, on(B,A) E KB
KB |-?- on(B,0)    - no explicit info in KB, so try reduction:
                      Replace x/0, y/A, z/B
                      on(A,0) ^ on(B,A) --> on(B,0)
                         But on(A,0) ^ on(B,A) E KB
                      So R "knows" on(B,0)

Resolution for Predicate Logic

From formulas of P.L. to Clauses

• Move quantifiers infront of the formula Q₁Q₂...Q_k α
• Remove quantifiers - Skolemization :
  AxAyEz (x<y) -> (x<z ^ z<y) will be: (x<y) -> (x<f(x,y) ∧ f(x,y)<y)
• Standard conversion into clauses (or CNF) - Need a unification algorithm

Unification Algorithm

Problem: 
Given 2 expressions (atomic formulas, terms, ...):
	l1(x1,...,xk) and 
	l2(x1,...,xk), 
Can we assign meanings to x1,...,xk 
such that
l1 and l2 are the same under this assignment?

Example:
X < 2      1 < y
l1(x,y)     l2(x,y)
if x = 1, y = 2 under this assignment.
x < 2 becomes 1 < 2
1 < y becomes 1 < 2

Substitution [x1/t1,...,xk/tk]
Let X = {l1,l2} A substition e is called
a unifier of X if e(l1) = e(l2)

Example:
Let l1 = x < 2, l2 = 1 < y
Let e = [x/1,y/2], Then
e(l1) = e(x < 2) = 1 < 2
e(l2) = e(1 < y) = 1 < 2
So, {l1,l2} is unifiable and e is a 
unifier of this set.

Unification Algorithm:

INPUT: {l1, l2} of atomic formulas

OUTPUT: A unifier e if this set is unifiable
	"Not unifable" otherwise

Can only substitute a variable with a term!

Resolution Rule:

C1 v l1, C2 v ¬l2, e(l1) = e(l2)
--------------------------------
         e(C1) v e(C2)

Example:
C1 = p(x,28) v r(f(x,7))
C2 = ¬q(x,28) v ¬r(f(g(2),y))

Is {r(f(x,7)),r(f(g(2),y))} Unifiable?
	e = [x/g(2),y/7]	YES

p(x,28) v r(f(x,7)), ¬q(x,28) v ¬r(f(g(2),y)), e(l1) = e(l2)

e(p(x,28)) v e(¬q(x,28)))
=
e(p(g(2),28)) v e(¬q(g(2),28))) Resolvent

Refutation of a set of clauses:
C₁,...,C_n
such that,
C_n is the empty clause
For every C_i: C_i E S or C_i = e(C_j), j < i (Renaming variables, factoring) or C_i is the resolvent of C_j, C_k, j,k < i

Fact1 (Logic): KB |-- α iff KB U {¬α}

Fact2 (Robinson): A set S of clauses is inconsistent iff it is refutatable using the resolution rule.

Fact2 (Logic+CS): It is undecidable wether or not a finite set S of clauses is refutation.

There is an algorithm that given a set S of clauses will output YES if S is inconsistent.

Planing.html >>>