CMPSC442-Wk6-Mtg16
Logical Agents
AIMA 7
CMPSC 442
Week 6, Meeting 16, 4 Segments
Outline
● Logical Agents, and Wumpus World
● Propositional Logic
● Theorem Proving
● Model Checking
2Outline, Wk 6, Mtg 16
Logical Agents
AIMA 7
CMPSC 442
Week 6, Meeting 16, Segment 1 of 4: Logical Agents and
Wumpus World
Agents with Explicit Knowledge Representation
● Knowledge base = set of sentences (declarations) in a formal language
● Adding to the KB
○ Agent Tells the KB what it perceives: S
i
○ Inference: derive new statements from KB + S
i
● Using the KB
○ Agent Asks the KB what action to take
○ Declaration of the action to take
4Logical Agents & Wumpus World
Generic KB Agent
5Logical Agents & Wumpus World
PEAS Description of Wumpus World
● Performance measure
○ gold +1000, death -1000
○ -1 per step, -10 for using the arrow
● Environment
○ Squares adjacent to wumpus are smelly
○ Squares adjacent to pit are breezy
○ Glitter iff gold is in the same square
○ Shooting kills wumpus if you are facing it
○ Shooting uses up the only arrow
○ Grabbing picks up gold if in same square
○ Releasing drops the gold in same square
○ Agent dies if entering a pit or a cell with a live wumpus
● Actuators: Left, Right, Up, Down, Grab, Release, Shoot
● Sensors: Stench, Breeze, Glitter, Bump, Scream
6Logical Agents & Wumpus World
Wumpus world characterization
● Partially Observable: Only local perception
● Deterministic: Action outcomes are exactly specified
● Non-episodic: Sequential at the level of actions
● Static: Wumpus and Pits do not change while agent decides on action
● Discrete
● Single-agent
7Logical Agents & Wumpus World
Exploring Wumpus World: an Initial Action
● Figure (a):
○ Agent in [1,1]
○ Percept:
[None,None,None,None,None]
○ Inferences added to KB: [1,2] is OK;
[2,1] is OK
● Figure (b):
○ Actuator: Right ￫ Agent in [2,1]
○ Percept:
[None,Breeze,None,None,None]
○ Inferences added to KB: ?Pit in
[2,2]; ?Pit in [3,1]
8Logical Agents & Wumpus World
● Figure (a):
○ Left ￫ Agent in [1,1]
○ Up ￫ Agent in [1,2]
○ Percept:
[Stench,None,None,None,None]
○ Inferences added to KB: [2,2] is OK
(not ?Pit in [2,2]); Wumpus in [1,3]
● Figure (b):
○ Right ￫ Agent in [2,2]
○ Up ￫ Agent in [2,3]
○ Percept: [Stench, Breeze, Glitter,None,None]
○ Inferences added to KB: Gold in [2,3]; ?P in [2,4]; ?P in [3,3]
Exploring Wumpus World:
9Logical Agents & Wumpus World
Formalizing the KB
● Wumpus world illustrates a logical agent: the agent takes an action,
which results in a new percept, leading to new facts to add to the KB
○ Facts can follow directly from percepts
○ Facts can follow from other facts
● How could such an agent be implemented?
○ A logic language provides a way to represent and reason about facts
○ Predicate logic is introduced next as a first step
10Logical Agents & Wumpus World
General Properties of a Logical Formalism
● Logic: a way to formulate statements, interpret them, and derive
conclusions
○ Syntax: vocabulary, rules of combination to make statements
○ Semantics: truth of statements in possible worlds, or models
○ Entailment: a way to evaluate consistency of models with one another
11Logical Agents & Wumpus World
Models
● A logical model m is a formally structured world 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 α
● Entailment:
○ KB ⊨ α iff M(KB) ⊆ M(α)
○ Example:
● KB = Giants won and Reds lost
● α = Giants won
12Logical Agents & Wumpus World
Entailment in Wumpus World
● Agent in [1,1], Percept [N,N,N,N,N]
● Right ￫ Agent [2,1], Percept [N,B,N,N,N]
● Eight possibilities for [1,2], [2,2], [3,1]
13Logical Agents & Wumpus World
Model Checking and Wumpus World
● 8 possible worlds
○ 3 (in red) consistent with
Agent in [2,1] [N,B,N,N,N,N]
○ Statement to check: α1 ([1,2] is
safe])
○ KB ⊨ α1
14Logical Agents & Wumpus World
Model Checking and Wumpus World
15
● 8 possible worlds
○ 3 (in red) consistent with
Agent in [2,1] [N,B,N,N,N,N]
○ Statement to check: α2 ([2,2] is
safe])
○ KB ⊭α2
Logical Agents & Wumpus World
Logical Agents
AIMA 7
CMPSC 442
Week 6, Meeting 16, Segment 2 of 4: Propositional Logic
Propositional Logic
● Simple sentences symbols are atomic, non-decomposable: A, B
● Logical operators combine simple sentences into complex sentences
○ ¬A (not A)
○ A ∧ B (A and B)
○ A ∨ B (A or B)
○ A ⇒ B (if A then B)
○ A ⇔ B (A entails B)
● Sentences are true or false
17Propositional Logic
Operator Precedence
● Unary operators (¬) precede binary operators (∧∨⇒⇔)
● Conjunction and disjunction (∧∨) precede conditionals (⇒⇔)
● Conjunction (∧) precedes disjunction (∨)
● Implication (⇒) precedes biconditional (⇔)
18Propositional LogicPropositional Logic
Syntax of Propositional Logic
The proposition symbols P
1
, P
2
etc are sentences
● If S is a sentence, ¬S is a sentence (negation)
● If S
1
and S
2
are sentences, S
1
∧ S
2
is a sentence (conjunction)
● If S
1
and S
2
are sentences, S
1
∨ S
2
is a sentence (disjunction)
● If S
1
and S
2
are sentences, S
1
⇒ S
2
is a sentence (implication)
● If S
1
and S
2
are sentences, S
1
⇔ S
2
is a sentence (biconditional)
19Propositional Logic
Backus-Naur Form
20Propositional Logic
Translating between Propositions and English
21
Propositional
Logic
English
A Today is a holiday.
B We are going to the zoo.
A ⇒ B If today is a holiday, we are going to the zoo.
A ∧ ¬ B Today is a holiday and we’re not going to the zoo.
¬ A ⇒ ¬ B If today is not a holiday, we’re not going to the zoo.
¬ B ⇒ ¬ A If we’re not going to the zoo, today is not a holiday.
B ⇒ A If we are going to the zoo, today is a holiday.
Propositional Logic
Truth Table for Connectives
● Columns are in precedence order
○ P ⇒ Q is true unless P is true and Q is false
○ P ⇔ Q is true iff P and Q are both true or both false
● For 3 statements (S
1
, S
2
, S
3
), 23 combinations of truth values = 8 models
● Recursive evaluation of arbitrary sentences. If P
1,2
= false, P
2,2
= true, P
1,2
= false:
○ ¬ P
1,2
∧ (P
2,2
∨ P
3,1
) = true ∧ (true ∨ false) = true ∧ true = true
22Propositional Logic
Wumpus World Sentences
● Let P
i,j
be true if there is a pit in [i, j]
● Let B
i,j
be true if there is a breeze in [i, j]
¬ P
1,1
¬ B
1,1
● Pits cause breezes in adjacent squares
B
1,1
⇔
(P
1,2
∨ P
2,1
)
B
2,1
⇔ (P
1,1
∨ P
2,2
∨ P
3,1
)
23Propositional Logic
Logical Agents
AIMA 7
CMPSC 442
Week 6, Meeting 16, Segment 3 of 4: Theorem Proving
Proof Methods: Roughly Two Kinds
● Natural Deduction: Application of inference rules
○ Legitimate (sound) generation of new sentences from old
○ Proof = a sequence of inference rule applications
■ Use inference rules as operators in a standard search algorithm
○ Typically requires transformation of sentences into a normal form
● Model checking
○ Truth table enumeration: for n propositional symbols, 0(2n)
○ Backtracking search, e.g., Davis-Putnam-Logemann-Loveland (DPLL)
○ Heuristic search in model space (sound but incomplete)
■ E.g., min-conflicts-like hill-climbing algorithms
25Theorem Proving
Logical Equivalence: Rewrite rules
26Theorem Proving
Validity and Satisfiability
● A sentence is valid if it is true in all models (tautologies; necessarily true)
○ e.g., A ∨¬A, A ⇒ A, (A ∧ (A ⇒ B)) ⇒ B
● Validity is connected to inference via the Deduction Theorem:
○ A ⊨ B if and only if (B ⇒ A) is valid
● A sentence is satisfiable if it is true in some model
○ e.g., A ∨ B
○ Determining satisfiability (the SAT problem) is NP-complete
● A sentence is unsatisfiable if it is true in no models
○ e.g., A∧¬A
● Satisfiability is connected to inference via reductio ad absurdum:
A ⊨ B if and only if (A ∧¬ B) is unsatisfiable
27Theorem Proving
Inference Rules
● Modus Ponens: if A is true, and A ⇒ B is true, then B is true
● And-Elimination
● Logical equivalence (rewrite) rules on slide 26
28Theorem Proving
Query a Wumpus KB: Prove ¬ P
1,2
29
Initial Facts
R
1
¬P
1,1
R
2
B
1,1
⇔ (P
1,2
∨ P
2,1
)
R
3
B
2,1
⇔ (P
1,1
∨ P
2,2
∨
P
3,1
)
R
4
¬ B
1,1
R
5
B
2,1
Inference/proof
R
2
, bicon. elim. R
6
:
(B
1,1
⇒ (P
1,2
∨ P
2,1
)) ∧ ((P
1,2
∨ P
2,1
) ⇒
B
1,1
)
R
6
, and-elim R
7
:
((P
1,2
∨ P
2,1
) ⇒ B
1,1
)
R
7
, contrapos. R
8
:
(¬ B
1,1
) ⇒ ¬ (P
1,2
∨ P
2,1
)
R
4,
R
8
, mod. pon. R
9
:
¬ (P
1,2
∨ P
2,1
)
R
9
, de Morgan R
10
:
¬ P
1,2
∧ ¬ P
2,1
Theorem Proving
Uninformed Search to Derive Proofs
● Initial State: The sentences in initial knowledge base
● Actions: Apply inference rules where a KB sentence matches the l.h.s.
● Result: Add r.h.s. of matched rules to KB
● Goal: A state containing the sentence to prove
Sound, but not necessarily complete with inference rules presented so far
● EG: If biconditional elimination is removed, then proof on slide 29 fails
● A more general inference rule could help fill in potential gaps
30Theorem Proving
Proof by Resolution
● Resolution: an inference rule that if coupled with a complete search
algorithm yields a complete inference algorithm
○ Inference rules covered above are all sound
○ Adding resolution yields completeness, if using a complete search
algorithm
31Theorem Proving
Unit Resolution: A First Step towards Completeness
● If (a ∨ ¬b) ∧ ¬a, then ¬b
● A disjunction of literals conjoined with the negation of one of the
disjuncts proves the other disjunct
● Called unit resolution because a single literal (e.g., c) can be viewed as
a disjunction of the literal (∨c), or a “unit clause”
● More generally expressed as:
32Theorem Proving
Resolution
● Generalization of unit resolution
● Two clauses can be combined to produce a new clause as follows
○ If the first clause contains a literal a, and the second clause contains its
negation ¬a
○ Then inference step is to produce a new single clause that includes all the
literals from both clauses except a and ¬a
33Theorem Proving
Resolution Requires Conjunctive Normal Form (CNF)
● The input to resolution consists of two clauses (implicit conjunction)
that are each disjunctions of literals
● To apply resolution, convert all propositions to conjunctive normal form
(CNF)
○ Apply bi-conditional elimination if applicable
○ Apply implication elimination if applicable
○ Move all ¬ inward to literals (double-negation elimination; de Morgan)
○ Apply distributivity of ∨ over ∧
34Theorem Proving
Resolution-based Theorem Prover
● For any sentences A and B in propositional logic, resolution can decide
whether A ⊨ B
● Step 1: Put the statements in conjunctive normal form (CNF)
● Step 2: Proof by contradiction
35Theorem Proving
Resolution Algorithm
36Theorem Proving
Example Proof
KB = (B1,1 ⇔ (P1,2 ∨ P2,1 )) ∧ ¬ B1,1
Prove: ¬ P1,2
CNF: (¬ P1,2 ∨ B1,1) ∧ (¬ B1,1 ∨ P1,2 ∨ P2,1) ∧ ( ¬ P2,1 ∨ B1,1) ∧ ¬ B1,1
37Theorem Proving
Logical Agents
AIMA 7
CMPSC 442
Week 6, Meeting 16, Segment 4 of 4: Model Checking
Efficient Model Checking Algorithms for PL
● Backward chaining (Horn Clauses)
● Forward chaining (Horn Clauses)
● DPLL Algorithm (Davis, Putnam, Logemann, Loveland)
○ Efficient and complete backtracking
○ Can efficiently handle tens of millions of variables
○ Applications include hardware verifiation
● WalkSAT
○ Local search, thus very efficient
○ Incomplete
39Model Checking
PL Forms: CNF, Horn Clauses, Definite Clauses
40Model Checking
Forward or Backward Chaining
● Require Horn Form
○ Conjunction of Horn clauses
○ Horn clauses: literal, or (conjunction of literals) ⇒literal
○ E.g., C
∧ (B ⇒ A)
∧ (C
∧ D ⇒ B)
● Modus Ponens (for Horn Form): complete for Horn KBs
● Forward chaining, linear time
● Backward chaining potentially much less than linear time
41Model Checking
Limitations of Propositional Logic
● Can only state specific truths
○ EG: B
2,1
● Cannot state generic truths
○ EG: cells next to pits are breezy
42Model Checking
Summary, Page One
● Logical agents apply inference to a KB to derive new facts and make
decisions
○ 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
43Summary Wk 6, Mtg 16 – 1
Summary, Page Two
● Resolution inference is complete for propositional logic
● Efficient search algorithms with inference procedures
○ Forward, backward chaining are linear-time, complete for Horn clauses
○ DPLL, recursive DFS; complete
○ WalkSAT: local search; very efficient, not complete
● Propositional logic has limited expressive power
44Summary Wk 6, Mtg 16 – 2