Chapter 7
Logical Agents  

powered by FreeFind

Modified: 

Outline

 

7.1 KNOWLEDGE-BASED AGENTS

Example: Vaccum world

Knowledge Base

Initially rules and facts (e.g. if Status==Dirty then Action=Suck)

TELL KB of percepts (e.g. Status=Dirty, Location=A) and inference (e.g. SuckClean)

ASK KB what to do based on rules and facts.
    Location==A and Status==Dirty
    if Status==Dirty then Action=Suck
    Action==SuckStatus=Clean

    Can deduce that:
        Location==A and Status==Clean

A generic knowledge-based agent

7.2 THE WUMPUS WORLD

Wumpus world PEAS description

 

Wumpus world characterization

 

Exploring the wumpus world

Other tight spots

  • Our agent starts in (1,1). How does she know that (1,2), (2,1) are OK also?
  • What does our agent learn by moving to (2,1), that is (column, row)?
  • When in (2,1) can she safely move to (2,2)?

 

7.3 Logic

Entailment

Models

Wumpus models

8 (23) possible models for pits in squares [1,2], [2,2] and [3,1]

 

Entailment in the wumpus world

Pit in [1,2], [2,2] and [3,1] can be True or False for any, 23.

Knowledge base

KB consists of wumpus world rules + observations:
     observations: breeze in [2,1] and nothing in [1,1]
     rules:            perceive breeze in squares directly adjacent to a pit

KB true in only 3 of the 8 models

More observations increase number of sentences in KB but do not invalidate previous. (e.g. learning that there is a breeze in [3,4] does not invalidate KB).

Model checking: enumerating all possible models (8) to verify that a1 is true in every model in which KB is true.

The sentence, there is no pit in [1,2], is true wherever KB is true. KB entails a1

In every model in which KB is true, cannot conclude the sentence a2, there is no pit in [2,2], nor conclude there is a pit in [2,2]

observations: breeze in [2,1] and nothing in [1,1]
rules:            perceive breeze in squares directly adjacent to a pit

 

Inference

 

Propositional logic: syntax

 

Propositional logic: semantics

The 8 models and KB entails a1

P1,2 P2,2 P3,1 KB a1
False False False False True
False False True True True
False True False True True
False True True True True
True False False False False
True False True False False
True True False False False
True True True False False

 

Does the above sentence define KB, a1 or both?

 

Truth tables for connectives

Note: biconditional is equivalence operation, P eq Q, P iff Q
         its inverse is exclusive or, P xor Q

 

Wumpus world sentences

 

Knowledge base in propositional logic sentences

Relevant KB after starting in [1,1] and moving to [2,1]. A breeze was perceived in [2,1]

R1 : P1,1        
R2 : B1,1(P1,2P2,1)       
R3 : B2,1(P1,1P2,2P3,1)
R4 : B1,1       
R5 : B2,1
R6 : P2,1
  

Let Si,j be true when square [i,j] is smelly.

Let Wi,j be true when square [i,j] is the wumpus.

  • What values are: S3,2 S2,3 S1,2
  • What values are: W3,2 W2,3 W1,3

For the rule  "squares adjacent to wumpus are smelly.

  • What is S1,2
  • What is the biconditional for S1,2
  • What is the biconditional for S2,2
  • What is W1,3
  • What is the biconditional for W1,3

The agent is in [1,1]

  • What sentences, in terms of W and S, are in the KB for the relevant squares? Include the percepts.

The agent moves to square [1,2].

  • What sentences, in terms of W and S, are included in the KB for the relevant squares? Include the percepts. 

KB after starting in [1,1] and moving to [2,1]

R1 : P1,1        
R2 : B1,1(P1,2P2,1)       
R3 : B2,1(P1,1P2,2P3,1)
R4 : B1,1       
R5 : B2,1
R6 : P2,1  

Truth tables for inference

KB contains

  • Draw all models for the wumpus in [1,3], [2,2] and [2,1], similar to that below.
  • Circle KB in terms of S and W after the agent moves from [1,1] to square [1,2].
  • Add a3, there is no wumpus in [2,1], to the drawing.
  • Does KB entail a3?
  • Add a4, there is no wumpus in [2,2], to the drawing.
  • Does KB entail a4?

A truth table consists of true and false assignments for every proposition symbol.

  • What symbols in terms of S and W are in KB?
  • How many models (i.e. rows) are required?
  • KB is true only when all sentences in KB are true. What are the row assignments in which KB is true?

KB after starting in [1,1] and moving to [2,1]

R1 : P1,1        
R2 : B1,1(P1,2P2,1)       
R3 : B2,1(P1,1P2,2P3,1)
R4 : B1,1       
R5 : B2,1
R6 : P2,1  

Inference by enumeration

Entails - A entails B if in every model that A is true, B is true.

Sound - Every sentence derived is logically valid or a tautology, only derives entailed sentences.

Complete - Can infer every sentence that logically follows from a set of sentences, can derive every entailed sentence.

Algorithm for inference by enumeration

Idea: Verify that for every model that KB is true, a is also true by generating truth table and checking KB and a for all symbols

TT-ENTAILS?(KB, a) returns true if KB entails a. Essentially enumerates at truth table checking that when KB is true a is true

TT-CHECK-ALL(KB, a, symbols, []) returns true if KB is false in model or if KB is true and a is true in the model. Recall checking that KB entails a, when KB is false a can be true or false, only must be true when KB is true.

PL-TRUE?(KB, model) returns true if KB is true in the model

PL-TRUE?(a, model) returns true if a is true in the model

EXTEND(P, true, model) returns a model with symbol P = true added.

EXTEND(P, false, model) returns a model with symbol P = false added.

 

Logical equivalence

Modus Ponens:   When ab and a are given,  b can be inferred

And-elimination: Given ab, either a or b can be inferred.
                       

Example of a logic proof: P1,2
        KB                                                Proof P1,2

R1 : P1,1    
R2 : B1,1( P1,2P2,1)
R3 : B2,1( P1,1P2,2P3,1)
R4 : B1,1  
R5 : B2,1   		R6 : B1,1( P1,2P2,1) biconditional elimination
      (B1,1( P1,2P2,1))(( P1,2P2,1)B1,1)
R7 : (( P1,2P2,1)B1,1)  And reduction of R6
R8 : (B1,1( P1,2P2,1)) Contraposition
R9 : ( P1,2P2,1) by Modus Ponens and percept B1,1
R10: P1,2P2,1 by de Morgan
Prove W2,1  

 

Validity and satisfiability


     

 

7.5 REASONING PATTERNS IN PROPOSITIONAL LOGIC

Proof methods

 

Resolution

Idea:    Proof by contradiction.
            Inference rule based on combining two disjunctive
            sentences containing complementary literals

      BA, B resolves to A

      BAC, BD resolves to ACD

 

Confirm or refute only

Resolution can determine whether P1,2P2,1 is true but cannot automatically derive true sentences.

Proof of soundness

Unit resolution

l1...lk,   m
_______________________
l1...li-1...li+1...lk

m and li are complementary.

m is given to be true, then li is false and l1...li-1...li+1...lk is still true because l1...lk was given to be true.
 

General resolution

l1...lk,   m1...mn
_______________________
l1...li-1...li+1...lkm1...mj-1...mj+1...mn

mj and li are complementary.

If mj is true then li is false and l1...li-1...li+1...lk is still true because l1...lk was given to be true.

If li is true then mj is false and m1...mj-1...mj+1...mn is still true because m1...mn was given to be true.
 

Conversion to CNF

Resolution applies only to disjunctions of literals

Every propositional logic sentence is equivalent to a conjunction of disjunction of literals, conjunctive normal form (CNF)

Example:

Convert to CNF:
  • AB
  • ABC

 

Resolution steps

  1. Put premises or axioms of KB in clause form (CNF)
  2. Add the negation to be proved, in clause form, to the KB
  3. Resolve clauses with complementary literals, producing new clauses that logically follow (sound).
  4. Continue until produce a contradiction of the clause to be proved by generating the empty clause.
  5. The substitutions used to produce the empty clause are those under which the opposite of the negated goal is true. That is, the results of the resolution substitutions leading to the contradiction are true; we can add to KB.

Example: Prove B

Given a KB of disjunctions

AB, CA, C   equivalent to (AB) (CA) C

  1. (AB) (CA) C
  2. (AB) (CA) C B
  3. Resolve
    1. (CA) with C is A
    2. A with (AB) is B
  4. B with B is empty clause
  5. (AB) (CA) C B A

 

Resolution algorithm

Discussion of resolution algorithm

KB: (AB) (CA) C
a: B

To prove KB entails a

  1. clauses = KBa = (AB) (CA) C B
  2. Loop
    • Resolve every pair of disjunctive clauses
    • e.g. (CA) with C
    • If resolution produces empty clause then return True
    • If no new clauses can be added return false

Example

B1,1(P1,2P2,1)B1,1
               (P2,1B1,1)(B1,1P1,2P2,1)(P1,2B1,1)B1,1   

Prove by contradiction: P1,2

KB P1,2

(P2,1B1,1)(B1,1P1,2P2,1)(P1,2B1,1)B1,1 P1,2

Resolve B1,1P1,2 with B1,1 result is P1,2

Resolve P1,2 with P1,2 result is empty clause

 

(P2,1B1,1)(B1,2P2,1)(P1,2B1,1)B1,1
  • Prove using resolution: P2,1
  • Prove using resolution: B1,2
Recall that:
    PB PB       and      PB  B P
Given KB:

   AB
   BCD

Use resolution to determine if the following conclusion is valid:

   AD

 

Give the KB in terms of S and W after
  • our agent starts at [1,1]
  • moves to [2,1]
  1. Give relevant sentences for KB in terms of S and W.
  2. How many rows are required in a truth table to prove entailment using enumeration?
  3. Prove, using resolution, W2,2

Note:
A(BCD)
(ABCD)(BA)(CA)(DA) 

 

Forward and backward chaining

Horn Clause

Disjunction of literals in which at most one is positive.

P2,1P1,1B1,1 is a Horn clause

B1,1 is a Horn clause (asserts a fact)

( P2,2P1,1) is a headless Horn clause or goals

P1,1B1,1 is not a Horn clause

 

Importance:

  1. Can be written as an implication:

        ( P2,2P1,1)B1,1 ( P2,2P1,1)B1,1

    where head is B1,1 and body is P2,2P1,1
  2. Inference through forward and backward chaining, to be discussed.
  3. Entailment can be done in linear time in the size of KB. Recall that enumeration was 2n.
Recall that:
    PB PB       and      PB  B P
Give the following as Horn clauses:
  1. B1,1P1,2
  2. (B1,1P1,2)
  3. P1,1B1,1
  4. ( P2,2P1,1)B1,1
  5. B1,1P1,2

 

Forward chaining

Prove Q

Facts                    Clauses

A, B                      ABL
A, B, L                  BLM
A, B, L, M              LMP
A, B, L, M, P          PQ
A, B, L, M, P, Q

Prove Z using forward chaining:
  1. RYX
  2. SXW
  3. RSX
  4. XWY
  5. YZ
  6. R
  7. S

Forward chaining algorithm

Example PL-FC-ENTAILS? operation to prove Q

agenda inferred[p] count[c] p c
A
B		 A   false
B   false
L   false
M  false
P   false
Q   false		 ABL      2
BLM      2
LMP      2
PQ           1		    
B A   true*
B   false
L   false
M  false
P   false
Q   false		 ABL      1*
BLM      2
LMP      2
PQ           1		 A ABL
L A   true
B   true*
L   false
M  false
P   false
Q   false		 ABL      0*
BLM      1*
LMP      2
PQ           1		 B ABL
BLM
M A   true
B   true
L   true*
M  false
P   false
Q   false		 ABL      0
BLM      0*
LMP      1
PQ           1		 L BLM
P A   true
B   true
L   true
M  true*
P   false
Q   false		 ABL      0
BLM      0
LMP      0*
PQ           1		 M LMP
  A   true
B   true
L   true
M  true
P   true*
Q   false		 ABL      0
BLM      0
LMP      0
PQ           0*		 P PQ

Q head
return true

Forward chaining example to prove Q

Proof of completeness

 

Backward chaining

 

Backward chaining example

Prove Q

Facts                Goals            Clauses

A, B                  Q                  PQ
A, B                  P,Q               LMP
A, B                  L,M,P,Q         ABL
A, B, L               M,P,Q           BLM
A, B, L, M           P,Q              LMP
A, B, L, M, P       Q                 PQ
A, B, L, M, P, Q 
         

Hazards in backward chaining

Notice if instead of selecting
ABL we select
APL the goal P is added back to the list of goals creating an infinite loop.

Facts                Goals            Clauses

A, B                  Q                  PQ
A, B                  P,Q               LMP
A, B                  L,M,P,Q         APL
A, B                  P*,L,M,P,Q    LMP

* Any backward chaining algorithm must avoid repeating goals; much as graph search maintains a closed-list of expanded states to avoid repetition, backward chaining can maintain a list of goals.

Prove Z using backward chaining:
  1. RYX
  2. SXW
  3. RSX
  4. XWY
  5. YZ
  6. R
  7. S

Backward chaining algorithm (Download)

goals=[]                                               # Current goals to satisfy     

def backchain(goal, rules, facts) :
   def clauseTrue(rule) :
      def symbolTrue(subgoal) :
         return backchain(subgoal, rules, facts)
      head = rule[0] 
      body = rule[1:]
      return (head == goal) and every(symbolTrue, body)
   if goal in facts : return True
   if goal in goals : return False               # Otherwise infinite loop
   goals.append(goal)
   result = some(clauseTrue, rules)
   goals.remove(goal)
   return result

def some(fn, list) :                                 # True if some fn(i) is True
   for i in list :
      if fn(i) : return True
   return False

def every(fn, list) :                                 # True if every fn(i) is True
   for i in list :
      if not fn(i) : return False
   return True
Example:  backchain( goal, rules, facts)

      backchain( q, [(q, p), (p, l, m), (m,b,l), (l,a,p), (l,a,b)], (a,b)) -> True

where APL is written as (l, a, p)
Discussion:
  • backchain( goal, rules, facts) returns True if the goal is True for the given rules and facts.
  • clauseTrue(rule) determines if a clause is True. Returns True if the rule head is the goal and all the symbols in the rule body are True. For example: APL has L head and symbols A and P in the body.
  • symbolTrue(subgoal) determines if a subgoal is True.
    For example: APL has L head and symbols A and P in the body; to prove L there are two subgoals, A and P.
  • some(fn, list) returns True if some fn(i) for i in list is True. Used to determine if some clause in the rules is True.
  • every(fn, list) returns True if every fn(i) for i in list is True. Used to determine if every symbol in the clause body is True; APL has L head and symbols A and P in the body; to prove L, A and P must both be True.
  • goals is the current list of goals (symbols) to prove True. A goal is added to the list before proving True and removed from the list after. The goal is allowed on the list of goals at several instances but only one at a time, otherwise looping can occur.

Backward chaining example

Forward chaining versus backward chaining

 

Summary