CSCE 420 Lecture 13

« previous | Tuesday, February 26, 2013 | next »

Midterm exam next week!

Wumpus World

4 × 4 Grid, Agent at starting position, pits and Wumpuses (foul-smelling creatures that will kill the agent) scattered throughout, goal is to find gold. Assume that Wumpuses cannot move.

• pits cause breeze in adjacent cells
• wumpuses cause stench in adjacent cells
• gold has a glitter in its own cell

Here might be a set of rules:

pickup_gold <- in(x,y) and glitter
go_north <- in(x,y) and not glitter and safe(x,y+1) and not visited(x,y+1)
safe(x,y) <- not wumpus(x,y) and not pit (x,y)
wumpus(x,y) <- stench(x+1,y) and stench(x-1,y) and stench(x,y+1) and stench(x,y-1)

Is it true that ${\text{facts}}\cup {\text{KB}}\models {\text{rule}}$?

• How do we answer a query?
• How do we decide entailments?

In general ${\text{KB}}\models q$ means "does $q$ follow from our knowledge base"

Entailment

Defined: KB entails $q$ if all the models of KB are a subset of all models of $q$

Brute-force: enumerate and check all models; is it decidable?

KB represented as a list of sentences, which are interpreted to all be conjoined with AND operations ${\text{KB}}=\left\{A\wedge B\implies C,\ A,\ \neg B\vee A\right\}$

Brute force:

$A$	$B$	$C$	$A\wedge B\implies C$	$\neg B\vee A$	KB
0	0	0	1	1	0
0	0	1	1	1	0
0	1	0	1	0	0
0	1	1	1	0	0
1	0	0	1	1	1
1	0	1	1	1	1
1	1	0	0	1	0
1	1	1	1	1	1

${\text{KB}}\models C$ is not true because a model that satisfies KB, namely $(A,B,C)=(1,0,0)$, does not satisfy $C$ (satisfiability is co-NPC)

Natural Deduction

Proof of $q$ from initial sentences KB by syntactic transformations

A finite-length proof is a sequence of sentences starting with KB and ending with $q$ such that each step is a sound derivation.

Logical equivalences are truth-preserving

$\neg (A\wedge B)\equiv \neg A\vee \neg B\quad \quad {\frac {\neg (A\wedge B)}{\neg A\vee \neg B}}\quad \quad \neg (A\wedge B)\vdash \neg A\vee \neg B$

The last symbol is read "derives" and may be subscripted with rule name.

Derivations may not be truth-preserving, but still represent sound transformations:

• AND-elimination: $A\wedge B\vdash A$
• Modus Ponens: $A\implies B,\ A\vdash A$
• Resolution: $P\vee Q,\ \neg P\vee R\vdash Q\vee R$

In general, a transformation is sound if $\alpha \vdash \beta$. This implies $\alpha \models \beta$

Algorithm

function NatDed(KB, q) returns Bool
  proof <- append(KB)
  while true
    select inference transformation
    select pair of sentences to which transformation applies
    create derived sentence by applying transformation
    if q = derived, return true
    proof.append(derived)
  end while
end function

Example Trace:

$P\implies Q,\ L\wedge M\implies P,\ B\wedge L\implies M,\ A\wedge B\implies L,\ A,\ B$ . . . $KB\models Q$ ?

1. $P\implies Q$
2. $L\wedge M\implies P$
3. $B\wedge L\implies M$
4. $A\wedge B\implies L$
5. $A$
6. $B$
7. $\neg P\vee Q$ [1, Implication elimination]
8. $A\wedge B$ [5, 6, AND introduction]
9. $L$ [4, Modus ponens]
10. $B\wedge L$ [6, 9, AND introduction]
11. $M$ [10, 3, Modus ponens]
12. $L\wedge M$ [9,11, AND introduction]
13. $P$ [2, 12, Modus ponens]
14. $Q$ [12, 1, Modus ponens]

Proof Tree (And-Or Tree)

Q  (P -> Q)
`-- P  (L && M -> P)
    |-- L  (A && B -> L)
    |   |-- A
    |   `-- B
    `-- M  (L && B -> M)
        |-- L  (A && B -> L)
        |   |-- A
        |   `-- B
        `-- B  (fact)

Forward Chaining

Working bottom-up on proof tree using only modus ponens

Agenda: pattern-matching to antecedents of rules to see which can be "activated"

Using above example:

1. A = {A, B}       Rule 4 is activated, add L
2. A = {A, B, L}       Rule 3 is activated, add M
3. A = {A, B, L, M}       Rule 2 is activated, add P
4. A = {A, B, L, M, P}       Rule 4 is activated, add Q
5. Done

Only restricted to Horn-Clause knowledge bases: disjunction with at most one positive literal

• (As opposed to conjunctive rules with all positive literals)
• $A\wedge B\implies C\equiv \neg A\vee \neg B\vee C$
• Won't work for ${\text{KB}}=\{P\vee Q,\ \neg P\}\models Q$

Algorithm

function Forward-Chaining(KB, q) returns Bool
  queue.push(facts(KB))
  for each r in literals(KB)
    count(r) := 0  (* number of antecedents of r  satisfied *)
  end for
  while queue is not empty
    p := queue.pop
    if p = q, return true
    else if inferred(p) = F then  (* not already on agenda *)
      inferred(p) = T
      for each rule r for which p in antecedents(r)
        count(r) := count(r) - 1
        if count(r) = 0, queue.push(consequence(r))
      end for
    end if
  end while
  return false
end function

Summary

Forward-Chaining and Natural Deduction can generate many irrelevant consequences

Tomorrow: Back-Chaining is a top-down ("goal-directed") approach that starts with query and works backwards to establish truth of query