Transcript Propositional logic

Knowledge and reasoning – second part
•
•
•
•
•
•
Knowledge representation
Logic and representation
Propositional (Boolean) logic
Normal forms
Inference in propositional logic
Wumpus world example
IES 503
1
Knowledge-Based Agent
• Agent that uses prior or acquired
knowledge to achieve its goals
Domain independent algorithms
ASK
Inference engine
TELL
Knowledge Base
Domain specific content
• Can make more efficient decisions
• Can make informed decisions
• Knowledge Base (KB): contains a set of
representations of facts about the Agent’s
environment
• Each representation is called a sentence
• Use some knowledge representation
language, to TELL it what to know e.g.,
(temperature 72F)
• ASK agent to query what to do
• Agent can use inference to deduce new
facts from TELLed facts
IES 503
2
Generic knowledge-based agent
1.
TELL KB what was perceived
Uses a KRL to insert new sentences, representations of facts, into KB
2.
ASK KB what to do.
Uses logical reasoning to examine actions and select best.
IES 503
3
Wumpus world example
IES 503
4
Wumpus world characterization
• Deterministic?
• Accessible?
• Static?
• Discrete?
• Episodic?
IES 503
5
Wumpus world characterization
• Deterministic?
Yes – outcome exactly specified.
• Accessible?
No – only local perception.
• Static?
Yes – Wumpus and pits do not move.
• Discrete?
Yes
• Episodic?
(Yes) – because static.
IES 503
6
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
7
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
8
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
9
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
10
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
11
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
12
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
13
Exploring a Wumpus world
A= Agent
B= Breeze
S= Smell
P= Pit
W= Wumpus
OK = Safe
V = Visited
G = Glitter
IES 503
14
Other tight spots
IES 503
15
Another example solution
No perception  1,2 and 2,1 OK
B in 2,1  2,2 or 3,1 P?
Move to 2,1
1,1 V  no P in 1,1
Move to 1,2 (only option)
IES 503
16
Example solution
S and No S when in 2,1  1,3 or 1,2 has W
1,2 OK  1,3 W
No B in 1,2  2,2 OK & 3,1 P
IES 503
17
Logic in general
IES 503
18
Types of logic
IES 503
19
The Semantic Wall
Physical Symbol System
World
+BLOCKA+
+BLOCKB+
+BLOCKC+
P1:(IS_ON +BLOCKA+ +BLOCKB+)
P2:((IS_RED +BLOCKA+)
IES 503
20
Truth depends on Interpretation
Representation 1
World
A
B
ON(A,B) T
ON(A,B) F
ON(A,B) F
A
ON(A,B) T
B
IES 503
21
Entailment
Entailment is different than inference
IES 503
22
Logic as a representation of the World
Representation: Sentences
entails
Sentence
Refers to
(Semantics)
World
Facts
IES 503
follows
Fact
23
Models
IES 503
24
Inference
IES 503
25
Basic symbols
• Expressions only evaluate to either “true” or “false.”
•
•
•
•
•
•
P
¬P
PVQ
P^Q
P => Q
PQ
“P is true”
“P is false”
negation
“either P is true or Q is true or both”
disjunction
“both P and Q are true”
conjunction
“if P is true, the Q is true”
implication
“P and Q are either both true or both false” equivalence
IES 503
26
Propositional logic: syntax
IES 503
27
Propositional logic: semantics
IES 503
28
Truth tables
• Truth value: whether a statement is true or false.
• Truth table: complete list of truth values for a statement given all
possible values of the individual atomic expressions.
Example:
P
T
T
F
F
Q
T
F
T
F
PVQ
T
T
T
F
IES 503
29
Truth tables for basic connectives
P Q
¬P
¬Q
PVQ
P ^ Q P=>Q PQ
T
T
F
F
F
F
T
T
F
T
F
T
T
T
T
F
T
F
F
F
T
F
T
F
IES 503
T
F
T
T
T
F
F
T
30
Propositional logic: basic manipulation rules
• ¬(¬A) = A
Double negation
• ¬(A ^ B) = (¬A) V (¬B)
• ¬(A V B) = (¬A) ^ (¬B)
Negated “and”
Negated “or”
•
•
•
•
•
•
Distributivity of ^ on V
by definition
using negated or
by definition
using negated and & or
A ^ (B V C) = (A ^ B) V (A ^ C)
A => B = (¬A) V B
¬(A => B) = A ^ (¬B)
A  B = (A => B) ^ (B => A)
¬(A  B) = (A ^ (¬B))V(B ^ (¬A))
…
IES 503
31
Propositional inference: enumeration method
IES 503
32
Enumeration: Solution
IES 503
33
Propositional inference: normal forms
“product of sums of
simple variables or
negated simple variables”
“sum of products of
simple variables or
negated simple variables”
IES 503
34
Deriving expressions from functions
• Given a boolean function in truth table form, find a propositional
logic expression for it that uses only V, ^ and ¬.
• Idea: We can easily do it by disjoining the “T” rows of the truth
table.
Example: XOR function
P
T
T
F
F
Q
T
F
T
F
RESULT
F
T
T
F
P ^ (¬Q)
(¬P) ^ Q
RESULT = (P ^ (¬Q)) V ((¬P) ^ Q)
IES 503
35
A more formal approach
• To construct a logical expression in disjunctive normal form from a
truth table:
- Build a “minterm” for each row of the table, where:
- For each variable whose value is T in that row, include
the variable in the minterm
- For each variable whose value is F in that row, include
the negation of the variable in the minterm
- Link variables in minterm by conjunctions
- The expression consists of the disjunction of all minterms.
IES 503
36
Example: adder with carry
Takes 3 variables in: x, y and ci (carry-in); yields 2 results: sum (s) and carryout (co). To get you used to other notations, here we assume T = 1, F =
0, V = OR, ^ = AND, ¬ = NOT.
co is:
s is:
IES 503
37
Tautologies
• Logical expressions that are always true. Can be simplified out.
Examples:
T
TVA
A V (¬A)
¬(A ^ (¬A))
AA
((P V Q)  P) V (¬P ^ Q)
(P  Q) => (P => Q)
IES 503
38
Validity and satisfiability
Theorem
IES 503
39
Proof methods
IES 503
40
Inference Rules
IES 503
41
Inference Rules
IES 503
42
Resolution
Conjunctive Normal Form (CNF)
•
conjunction of disjunctions of literals clauses
E.g., (A  B)  (B  C  D)
Resolution inference rule (for CNF):
li …  lk, m1  …  mn
li  …  li-1  li+1  …  lk  m1  …  mj-1  mj+1 ...  mn
where li and mj are complementary literals.
E.g., P1,3  P2,2, P2,2
P1,3
•
Resolution is sound and complete
for propositional logic
Conversion to CNF
B1,1  (P1,2  P2,1)
1)
Eliminate , replacing α  β with (α  β)(β  α).
2)
Eliminate , replacing α  β with α β.
3)
Move  inwards using de Morgan's rules and double-negation:
4)
Apply distributivity law ( over ) and flatten:
(B1,1  (P1,2  P2,1))  ((P1,2  P2,1)  B1,1)
(B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
(B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
(B1,1  P1,2  P2,1)  (P1,2  B1,1)  (P2,1  B1,1)
Resolution algorithm
• Proof by contradiction, i.e., show KBα unsatisfiable
Resolution example
• KB = (B1,1  (P1,2 P2,1))  B1,1
•
α = P1,2
Forward and backward chaining
• Horn Form (restricted)
KB = conjunction of Horn clauses
• Horn clause =
• proposition symbol; or
• (conjunction of symbols)  symbol
• E.g., C  (B  A)  (C  D  B)
•
• Modus Ponens (for Horn Form): complete for Horn KBs
α 1  …  αn  β
α1, … ,αn
β
• Can be used with forward chaining or backward chaining.
• These algorithms are very natural and run in linear time
Forward chaining
• Idea: fire any rule whose premises are satisfied in the
KB,
• add its conclusion to the KB, until query is found
Forward chaining algorithm
• Forward chaining is sound and complete for
Horn KB
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Proof of completeness
•
FC derives every atomic sentence that is
entailed by KB
1. FC reaches a fixed point where no new atomic
sentences are derived
2. Consider the final state as a model m, assigning
true/false to symbols
3. Every clause in the original KB is true in m
a1  …  ak  b
4. Hence m is a model of KB
5. If KB╞ q, q is true in every model of KB, including
m
Backward chaining
Idea: work backwards from the query q:
to prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal
stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Forward vs. backward 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
• 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
Efficient propositional inference
Two families of efficient algorithms for propositional
inference:
Complete backtracking search algorithms
• DPLL algorithm (Davis, Putnam, Logemann, Loveland)
• Incomplete local search algorithms
• WalkSAT algorithm
The DPLL algorithm
Determine if an propositional logic sentence (in CNF) is satisfiable.
Improvements over truth table enumeration:
1. Early termination
A clause is true if any literal is true.
A sentence is false if any clause is false.
2. Pure symbol heuristic
Pure symbol: always appears with the same "sign" in all clauses.
e.g., In the three clauses (A  B), (B  C), (C  A), A and B are pure, C is
impure.
Make a pure symbol literal true.
3. Unit clause heuristic
Unit clause: only one literal in the clause
The only literal in a unit clause must be true.
The DPLL algorithm
The WalkSAT algorithm
• Incomplete, local search algorithm
• Evaluation function: The min-conflict heuristic of
minimizing the number of unsatisfied clauses
• Balance between greediness and randomness
The WalkSAT algorithm
Inference-based agents in the wumpus world
A wumpus-world agent using propositional logic:
P1,1
W1,1
Bx,y  (Px,y+1  Px,y-1  Px+1,y  Px-1,y)
Sx,y  (Wx,y+1  Wx,y-1  Wx+1,y  Wx-1,y)
W1,1  W1,2  …  W4,4
W1,1  W1,2
W1,1  W1,3
…
 64 distinct proposition symbols, 155 sentences
Wumpus world: example
• Facts: Percepts inject (TELL) facts into the KB
• [stench at 1,1 and 2,1]  S1,1 ; S2,1
• Rules: if square has no stench then neither the square
or adjacent square contain the wumpus
• R1: !S1,1 !W1,1  !W1,2  !W2,1
• R2: !S2,1 !W1,1 !W2,1  !W2,2  !W3,1
• …
• Inference:
• KB contains !S1,1 then using Modus Ponens we infer
!W1,1  !W1,2
 !W2,1
• Using And-Elimination we get: !W1,1
• …
IES 503
!W1,2
!W2,1
78
Limitations of Propositional Logic
1. It is too weak, i.e., has very limited expressiveness:
• Each rule has to be represented for each situation:
e.g., “don’t go forward if the wumpus is in front of you” takes 64
rules
2. It cannot keep track of changes:
• If one needs to track changes, e.g., where the agent has been
before then we need a timed-version of each rule. To track 100
steps we’ll then need 6400 rules for the previous example.
Its hard to write and maintain such a huge rule-base
Inference becomes intractable
IES 503
79
Summary
IES 503
80