Logic Agents and Propositional
Logic
            CHAPTER 7
         HASSAN KHOSRAVI
            SPRING2011
                     Knowledge-Based Agents
 KB = knowledge base
   A set of sentences or facts
   e.g., a set of statements in a logic language
 Inference
   Deriving new sentences from old
   e.g., using a set of logical statements to infer new ones
 A simple model for reasoning
   Agent is told or perceives new evidence
         E.g., A is true
     Agent then infers new facts to add to the KB
         E.g., KB = { A -> (B OR C) }, then given A and not C we can infer that B is true
         B is now added to the KB even though it was not explicitly asserted, i.e., the
          agent inferred B
                       Wumpus World
 Environment
   Cave of 4×4
   Agent enters in [1,1]
   16 rooms
     Wumpus: A deadly beast who kills anyone
      entering his room.
     Pits: Bottomless pits that will trap you
      forever.
     Gold
                     Wumpus World
 Agents Sensors:
   Stench next to Wumpus
   Breeze next to pit
   Glitter in square with gold
   Bump when agent moves into a wall
   Scream from wumpus when killed
 Agents actions
   Agent can move forward, turn left or
    turn right
   Shoot, one shot
                     Wumpus World
 Performance measure
   +1000 for picking up gold
   -1000 got falling into pit
   -1 for each move
   -10 for using arrow
         Reasoning in the Wumpus World
 Agent has initial ignorance about the configuration
    Agent knows his/her initial location
    Agent knows the rules of the environment
 Goal is to explore environment, make inferences
 (reasoning) to try to find the gold.
 Random instantiations of this problem used to test agent
 reasoning and decision algorithms
 (applications? “intelligent agents” in computer games)
           Exploring the Wumpus World
[1,1] The KB initially contains the rules of the environment.
The first percept is [none, none,none,none,none],
move to safe cell e.g. 2,1
           Exploring the Wumpus World
[2,1] = breeze
   indicates that there is a pit in [2,2] or [3,1],
   return to [1,1] to try next safe cell
          Exploring the Wumpus World
[1,2] Stench in cell which means that wumpus is in [1,3] or [2,2]
   YET … not in [1,1]
   YET … not in [2,2] or stench would have been detected in [2,1]
           (this is relatively sophisticated reasoning!)
          Exploring the Wumpus World
[1,2] Stench in cell which means that wumpus is in [1,3] or [2,2]
    YET … not in [1,1]
    YET … not in [2,2] or stench would have been detected in [2,1]
           (this is relatively sophisticated reasoning!)
   THUS … wumpus is in [1,3]
   THUS [2,2] is safe because of lack of breeze in [1,2]
   THUS pit in [1,3] (again a clever inference)
   move to next safe cell [2,2]
           Exploring the Wumpus World
[2,2] move to [2,3]
[2,3] detect glitter , smell, breeze
   THUS pick up gold
   THUS pit in [3,3] or [2,4]
           What our example has shown us
 Can represent general knowledge about an environment by a
  set of rules and facts
 Can gather evidence and then infer new facts by combining
  evidence with the rules
 The conclusions are guaranteed to be correct if
   The evidence is correct
   The rules are correct
   The inference procedure is correct
    -> logical reasoning
 The inference may be quite complex
   E.g., evidence at different times, combined with different rules, etc
                               What is a Logic?
 A formal language
   KB = set of sentences
 Syntax
   what sentences are legal (well-formed)
   E.g., arithmetic
         X+2 >= y is a wf sentence, +x2y is not a wf sentence
 Semantics
   loose meaning: the interpretation of each sentence
   More precisely:
         Defines the truth of each sentence wrt to each possible world
     e.g,
         X+2 = y is true in a world where x=7 and y =9
         X+2 = y is false in a world where x=7 and y =1
     Note: standard logic – each sentence is T of F wrt eachworld
         Fuzzy logic – allows for degrees of truth.
                  Models and possible worlds
 Logicians typically think in terms of models, which are formally
  structured worlds with respect to which truth can be evaluated.
 m is a model of a sentence          if  is true in m
 M() is the set of all models of 
 Possible worlds ~ models
     Possible worlds: potentially real environments
     Models: mathematical abstractions that establish the truth or falsity of every
      sentence
 Example:
     x + y = 4, where x = #men, y = #women
     Possible models = all possible assignments of integers to x and y
                      Entailment
 One sentence follows logically from another
       |= b
   entails sentence b if and only if b is true in all
 worlds where  is true.
               e.g., x+y=4 |= 4=x+y
 Entailment is a relationship between sentences that
 is based on semantics.
            Entailment in the wumpus world
   Consider possible models for KB assuming only pits and a reduced Wumpus
    world
   Situation after detecting nothing in [1,1], moving right, detecting breeze in
    [2,1]
                Wumpus models
All possible models in this reduced Wumpus world.
              Wumpus models
 KB = all possible wumpus-worlds consistent
 with the observations and the “physics” of the
 Wumpus world.
                     Inferring conclusions
 Consider 2 possible conclusions given a KB
      α1 = "[1,2] is safe"
      α2 = "[2,2] is safe“
 One possible inference procedure
      Start with KB
      Model-checking
           Check if KB ╞  by checking if in all possible models where KB is
            true that  is also true
 Comments:
      Model-checking enumerates all possible worlds
           Only works on finite domains, will suffer from exponential growth
            of possible models
                                Wumpus models
α1 = "[1,2] is safe", KB ╞ α1, proved by model checking
                 Wumpus models
α2 = "[2,2] is safe", KB ╞ α2
There are some models entailed by KB where 2 is
 false
                              Logical inference
 The notion of entailment can be used for logic inference.
     Model checking (see wumpus example): enumerate all possible
      models and check whether  is true.
 If an algorithm only derives entailed sentences it is called
  sound or truth preserving.
     Otherwise it just makes things up.
      i is sound if whenever KB |-i  it is also true that KB|= 
     E.g., model-checking is sound
 Completeness : the algorithm can derive any sentence
  that is entailed.
  i is complete if whenever KB |=  it is also true that KB|-i 
           Schematic perspective
If KB is true in the real world, then any sentence  derived
from KB by a sound inference procedure is also true in the
real world.
                  Propositional logic: Syntax
 Propositional logic is the simplest logic – illustrates basic ideas
 Atomic sentences = single proposition symbols
   E.g., P, Q, R
   Special cases: True = always true, False = always false
 Complex sentences:
     If S is a sentence, S is a sentence (negation)
     If S1 and S2 are sentences, S1  S2 is a sentence (conjunction)
     If S1 and S2 are sentences, S1  S2 is a sentence (disjunction)
     If S1 and S2 are sentences, S1  S2 is a sentence (implication)
     If S1 and S2 are sentences, S1  S2 is a sentence (biconditional)
                Propositional logic: Semantics
Each model/world specifies true or false for each proposition symbol
   E.g.    P1,2      P2,2         P3,1
           false     true         false
   With these symbols, 8 possible models, can be enumerated automatically.
Rules for evaluating truth with respect to a model m:
           S        is true iff S is false
          S1  S2 is true iff    S1 is true and         S2 is true
          S1  S2 is true iff    S1is true or           S2 is true
          S1  S2 is true iff S1 is false or            S2 is true
              i.e., is false iff S1 is true and         S2 is false
          S1  S2     is true iff S1S2 is true andS2S1 is true
Simple recursive process evaluates an arbitrary sentence, e.g.,
                 P1,2  (P2,2  P3,1) = true  (true  false) = true  true = true
Truth tables for connectives
  Truth tables for connectives
Implication is always true
when the premise is false
Why? P=>Q means “if P is true then I am claiming that Q is true,
                  otherwise no claim”
Only way for this to be false is if P is true and Q is false
                      Wumpus world sentences
Let Pi,j be true if there is a pit in [i, j].
Let Bi,j be true if there is a breeze in [i, j].
    start:    P1,1
                          B1,1
                           B2,1
   "Pits cause breezes in adjacent squares"
    B1,1  (P1,2  P2,1)
    B2,1  (P1,1  P2,2  P3,1)
   KB can be expressed as the conjunction of all of these sentences
   Note that these sentences are rather long-winded!
       E.g., breese “rule” must be stated explicitly for each square
       First-order logic will allow us to define more general relations (later)
Truth tables for the Wumpus KB
              Inference by enumeration
 We want to see if  is entailed by KB
 Enumeration of all models is sound and complete.
 But…for n symbols, time complexity is O(2n)...
 We need a more efficient way to do inference
    But worst-case complexity will remain exponential for
     propositional logic
                          Logical equivalence
 To manipulate logical sentences we need some rewrite rules.
 Two sentences are logically equivalent iff they are true in same models: α ≡ ß iff α╞ β and
  β╞ α
 Modus Ponens
 And-Elimination
 Bi-conditional Elimination
               Validity and satisfiability
A sentence is valid if it is true in all models,
  e.g., True,   A A, A  A, (A  (A  B))  B
  (tautologies)
Validity is connected to inference via the Deduction
  Theorem:
  KB ╞ α if and only if (KB  α) is valid
A sentence is satisfiable if it is true in some model
  e.g., A B,   C
  (determining satisfiability of sentences is NP-complete)
A sentence is unsatisfiable if it is false in all models
  e.g., AA
Satisfiability is connected to inference via the following:
  KB ╞ α if and only if (KB α) is unsatisfiable
  (there is no model for which KB=true and  is false)
  (aka proof by contradiction: assume  to be false and this leads to
     contraditions in KB)
                                  Proof methods
   Proof methods divide into (roughly) two kinds:
    Application of inference rules:
       Legitimate (sound) generation of new sentences from old.
        Resolution
        Forward & Backward chaining
    Model checking
       Searching through truth assignments.
        Improved backtracking: Davis--Putnam-Logemann-Loveland (DPLL)
        Heuristic search in model space: Walksat.
                            Normal Form
  We want to prove: KB | 
                       equivalent to : KB   unsatifiable
  We first rewrite KB   into conjunctive normal form (CNF).
                                                                 literals
                               A “conjunction of disjunctions”
                                (A  B)  (B  C  D)
                                  Clause       Clause
• Any KB can be converted into CNF
• k-CNF: exactly k literals per clause
                    Example: Conversion to CNF
B1,1  (P1,2  P2,1)
1.   Eliminate , replacing α  β with (α  β)(β  α).
     (B1,1  (P1,2  P2,1))  ((P1,2  P2,1)  B1,1)
2. Eliminate , replacing α  β with α β.
     (B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
3. Move  inwards using de Morgan's rules and double-negation:
     (B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
4. Apply distributive law ( over ) and flatten:
     (B1,1  P1,2  P2,1)  (P1,2  B1,1)  (P2,1  B1,1)
         Resolution Inference Rule for CNF
(A  B  C )         “If A or B or C is true, but not A, then B or C
( A )               must be true.”
 (B  C )
                     “If A is false then B or C must be true,
(A  B  C )          or if A is true then D or E must be true,
                     hence since A is either true or false, B or C
( A  D  E )
                     or D or E must be true.”
 (B  C  D  E )
(A  B )
( A  B )                   Simplification
 (B  B )  B
              Resolution Algorithm
•   The resolution algorithm tries to prove:KB |  equivalent to
                                            KB   unsatisfiable
•   Generate all new sentences from KB and the query.
•   One of two things can happen:
1. We find P  P which is unsatisfiable,
                i.e. we can entail the query.
2. We find no contradiction: there is a model that satisfies the
    Sentence (non-trivial) and hence we cannot entail the query.
               KB  
                 Resolution example
 KB = (B1,1  (P1,2 P2,1))  B1,1
 α = P1,2
                             KB  
      True
                                       False in
                                       all worlds
                                Horn Clauses
• Resolution in general can be exponential in space and time.
• If we can reduce all clauses to “Horn clauses” resolution is linear in space and time
    A clause with at most 1 positive literal.
    e.g. A  B  C
    • Every Horn clause can be rewritten as an implication with
     a conjunction of positive literals in the premises and a single
     positive literal as a conclusion.
    e.g. B  C  A
    • 1 positive literal: definite clause
    • 0 positive literals: Fact or integrity constraint:
      e.g. (A  B )  (A  B  False )
Forward-chaining pseudocode
         Forward chaining: graph representation
 Idea: fire any rule whose premises are satisfied in the
     KB,
        add its conclusion to the KB, until query is found
                                                              AND gate
                          OR gate
 •       Forward chaining is sound and complete for Horn KB
         Forward chaining example
  “OR” Gate
“AND” gate
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
                     Forward chaining
 FC is data-driven, automatic, unconscious
 processing,
    e.g., object recognition, routine decisions
 May do lots of work that is irrelevant to the goal
                        Backward chaining
Idea: work backwards from the query q
           check if q is known already, or
           prove by BC all premises of some rule concluding q
           Hence BC maintains a stack of sub-goals that need to be proved to get to q.
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
                      we need P to prove
                      L and L to prove P.
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
                           Backward chaining
 BC is goal-driven, appropriate for problem-solving,
   e.g., Where are my keys? How do I get into a PhD program?
 Complexity of BC can be much less than linear in size of KB
Avoid loops: check if new sub-goal is already on the goal stack
Avoid repeated work: check if new sub-goal
    1.   has already been proved true, or
    2.   has already failed
Like FC, is linear and is also sound and complete (for Horn KB)
                 Model Checking
Two families of efficient algorithms:
 Complete backtracking search algorithms: DPLL
 algorithm
 Incomplete local search algorithms
   WalkSAT algorithm
                Satisfiability problems
 Consider a CNF sentence, e.g.,
 (D  B  C)  (B  A  C)  (C  B  E) 
 (E  D  B)  (B  E  C)
 Satisfiability: Is there a model consistent with this sentence?
 [A  B]  [¬B  ¬C]  [A  C]  [¬D]  [¬D  ¬A]
                     The WalkSAT algorithm
 Incomplete, local search algorithm
   Begin with a random assignment of values to symbols
   Each iteration: pick an unsatisfied clause
         Flip the symbol that maximizes number of satisfied clauses, OR
         Flip a symbol in the clause randomly
 Trades-off greediness and randomness
 Many variations of this idea
 If it returns failure (after some number of tries) we cannot
  tell whether the sentence is unsatisfiable or whether we
  have not searched long enough
     If max-flips = infinity, and sentence is unsatisfiable, algorithm never
      terminates!
 Typically most useful when we expect a solution to exist
Pseudocode for WalkSAT
             Hard satisfiability problems
 Consider random 3-CNF sentences. e.g.,
 (D  B  C)  (B  A  C)  (C  B  E) 
 (E  D  B)  (B  E  C)
 m = number of clauses (5)
 n = number of symbols (5)
    Underconstrained problems:
      Relatively few clauses constraining the variables
      Tend to be easy
      16 of 32 possible assignments above are solutions
        (so 2 random guesses will work on average)
              Hard satisfiability problems
 What makes a problem hard?
   Increase the number of clauses while keeping the number of
    symbols fixed
   Problem is more constrained, fewer solutions
     Investigate experimentally….
P(satisfiable) for random 3-CNF sentences, n
                      = 50
         Run-time for DPLL and WalkSAT
   Median runtime for 100 satisfiable random 3-CNF sentences, n = 50
Inference-based agents in the wumpus world
A wumpus-world agent using propositional logic:
 P1,1 (no pit in square [1,1])
 W1,1 (no Wumpus in square [1,1])
 Bx,y  (Px,y+1  Px,y-1  Px+1,y  Px-1,y) (Breeze next to Pit)
 Sx,y  (Wx,y+1  Wx,y-1  Wx+1,y  Wx-1,y) (stench next to Wumpus)
 W1,1  W1,2  …  W4,4 (at least 1 Wumpus)
 W1,1  W1,2 (at most 1 Wumpus)
 W1,1  W8,9
 …
 64 distinct proposition symbols, 155 sentences
Limited expressiveness of propositional logic
   KB contains "physics" sentences for every single square
    For every time t and every location [x,y],
    Lx,y  FacingRightt  Forwardt  Lx+1,y
   Rapid proliferation of clauses.
    First order logic is designed to deal with this through the
    introduction of variables.
                                Summary
 Logical agents apply inference to a knowledge base to derive new
  information and make decisions
 Basic concepts of logic:
     syntax: formal structure of sentences
     semantics: truth of sentences wrt models
     entailment: necessary truth of one sentence given another
     inference: deriving sentences from other sentences
     soundness: derivations produce only entailed sentences
     completeness: derivations can produce all entailed sentences
 Resolution is complete for propositional logic
 Forward, backward chaining are linear-time, complete for Horn clauses
 Propositional logic lacks expressive power