COSC 3402 Artificial Intelligence

<<< Using logic to implement goal-oriented behaviour

Proof by Resolution

Resolution only works on clauses.

We have two clauses: C₁ v p and C₂ v ¬p. But p and ¬p can not be true at the same time thus C₁ v C₂ must be true. The later is called the resolvent upon p.

Ex: p v ¬q, ¬p v q
    Resolve upon p: ¬q v q
    Resolve upon q: p v ¬p

Fact: The resolution rule is valid, i.e. if there exists a truth-value assignment h, such that h(C₁) = h(C₂) = 1 then h(resolvent_of(C₁,C₂)) = 1.

Proof: Suppose that
h(C1) = h(C2) = 1
and that
    C1 = A v p
    C2 = B v ¬p
We want to show that h(A v B) = 1

Case1: Suppose h(p) = 1, so h(¬p) = 0
       Since h(C2) = 1, we must have h(B) = 1
       So, h(A v B) = 1

Case2: Suppose h(p) = 0, so h(¬p) = 1
       Since h(C1) = 1, we must have h(A) = 1
       So, h(A v B) = 1

Definition: Let S be a set of clauses. A refutation of S is a sequence C₁, C₂, ..., C_n of clauses such that:

1. C_n is the empty clause (∅)
2. Every C_i in the sequence is either an element from S, or is the resolvent of some two clauses earlier in the sequence than C_i

Example:
S = {p v q, ¬p v q, p v ¬q, ¬p v ¬q}
    C1 = p v q (from S)
    C2 = ¬p v q (from S)
    C3 = q (resolvent of 1 and 2 upon p)
    C4 = p v ¬q (from S)
    C5 = ¬p v ¬q (from S)
    C6 = ¬q (resolvent of 4 and 5 upon p)
    C7 = ∅ (resolvent of 3 and 6 upon q)

Why is ∅ the same as the contradiction?
The only way to derive ∅ by a single application of the solution rule is to resolve l with ¬l.

Refutation tree

pvq  ¬pvq   pv¬q   ¬pv¬q
 \     /     \       /
  \   /       \     /
   \ /         \   /
    q           ¬q
    \           /
     \         /
      \       /
       \     /
        \   /
         \ /
          ∅

Objective: Implement KB|--_PC α

Fact1: KB |--_PC α iff KB U {¬α} is inconsistent (Principle of Contradiction)
e.g. {p} |-- P iff P U {¬p} = {p, ¬p}

Fact2: A set S of clauses is incosistent iff S can be refuted (A. Robinson)

To answer KB |--_PC α using resolution, we do the following:

1. Create KB U {¬α}
2. Convert KB U {¬α} into clauses (set S)
3. If S is refutable by resolution, then KB |--_PC α, otherwise KB |-/-_PC α

Level Saturation Algorithm

INPUT: KB - Set of formulas
       α - a formula

OUTPUT: YES if KB|--α (plus a proof)
        NO if KB|-/-α

METHOD:
        Let S1 be a set of clauses optained from KB U {¬α}
        Let i = 1

    Step1: if ∅ E Si, then return YES (plus refutation of Si)
    Step2: Let Si+1 be Si union all resultents of clauses from Si
    Step3: if Si+1 = Si, then return NO
           else i = i + 1; go to step 1

/* The size of Si+1 can be exponentially larger than Si */


Example:

KB = {p --> q, q --> r, p}
     α = r
S1 = {¬p v q, ¬q v r, p, ¬r}

Step1: ∅ /E S1
Step2: S2 = S1 U {¬p v r, q, ¬q}
Step3: S1 =/= S2
Step1: ∅ /E S1
Step2: S3 = S2 U {∅}
Step3: S1 =/= S2
Step1: ∅ E S1    /* Return YES */

Let S be set of clauses and let C E S be tautological clause. Then:

Definition: If every literal of a clause C is in a clause D, then we say that C subsumes D.

Example:
    C = p v ¬s
    D = r v ¬t v ¬s v a v p

Proof 1: Suppose that S is inconsistent and that S-{D} is consistent.
    So there exists a truth-value assignment h, such that:
    (1) h(S-{D}) = {1}
    By (1), h(C) = 1. Since D = C v A, then
    (2) h(D) = 1
    However, h(S) = h(S-{D}) U {h(D)} =by(1 & 2)= {1}U{1} = {1}
    This means that S is consistant, contradiction with the above.

Proof 2: Now suppose that S is consistent. By the definition of consistency
    There is a truth-value assignment h such that h(S) = {1},
	S, h(S-{D}) = {1} ---> S-{D} is consistent.

Predicate Logic >>>