Transcript Propositional logic

Reasoning with
Propositional Logic
automated processing of a simple knowledge base
CD
Knowledge representation
 propositions: set of atomic statements
that may be true or false
 general knowledge: set of complex
sentences describing conditions
(constraints) on environment
 facts: data (from perceptions) about
specific state of environment
D Goforth - COSC 4117, fall 2006
2
Knowledge representation
 KB - knowledge base: conjunction of
general knowledge and facts
 model: assignment of true/false values
to the propositions so KB can be
determined to be true or false
NOTE: term “model” is not clearly defined
– sometimes, it means any assignment
to propositions; usually it means an
assignments so KB is true
D Goforth - COSC 4117, fall 2006
3





propositions: set of atomic statements that may be true or false
general knowledge: complex sentences describing conditions on environment
facts: data (from perceptions) about specific state of environment
KB - knowledge base: conjunction of general knowledge and facts
model: assignment of true/false values to the propositions
Agent
environment
facts
model
general
knowledge
propositions
general
knowledge
propositions
Agent sets true/false values of propositions
to make model(s) where
KB is consistent (true)
- these models represent “understanding”
D Goforth - COSC 4117, fall 2006
4
Knowledge representation
truth table
propositions
general knowledge
facts
P1 P2 P3 ...Pn
R1 R2 R3 ...Rm Rm+1 Rm+2 Rm+3 ...Rk
KB=ΛRi
t t
t
...t
t
f
f ...t
f
f
f
...f
f
t t
t
...f
f
f
t ...t
f
t
t
...f
f
t t t
...
...t
t
f
f ...t
f
f
f
...f
f
f t t
...
...f
t
t
t ...t
t
t
t
...t
t
f f
...f
t
f
f ...f
f
t
f
...f
f
f
D Goforth - COSC 4117, fall 2006
5





propositions: set of atomic statements that may be true or false
general knowledge: complex sentences describing conditions on environment
facts: data (from perceptions) about specific state of environment
KB - knowledge base: conjunction of general knowledge and facts
model: assignment of true/false values to the propositions
Agent
facts
model
general
knowledge
propositions
general
knowledge
propositions
Is GREEN in front of RED?
NO
D Goforth - COSC 4117, fall 2006
6
Agent
facts
model
general
knowledge
propositions
general
knowledge
propositions
Facts (from perception):
General knowledge (incomplete):
1. RED occludes ORANGE
•if (ORANGE occludes RED) then
(ORANGE inFrontOf RED)
2. ORANGE occludes GREEN
Propositions:
1. ORANGE inFrontOf RED
2. ORANGE inFrontOf GREEN
3. RED inFrontOf GREEN
4. RED inFrontOf ORANGE
•if (RED inFrontOf ORANGE) then
not(ORANGE inFrontOf RED)
•if (RED inFrontOf ORANGE) and
(ORANGE inFrontOf GREEN) then
(RED inFrontOf GREEN)
•etc…
5. GREEN inFrontOf RED
6. GREEN inFrontOf ORANGE
D Goforth - COSC 4117, fall 2006
7
Knowledge representation
truth table
propositions
general knowledge facts
KB=ΛRi
P1 P2 P3 ...P6
R1 R2 R3 ...Rm Rm+1 Rm+2
t t t
...
...t
t
f
f ...t
t
t
f
f t t
...
...f
t
t
t ...t
t
t
t
f f
...f
t
f
f ...f
t
t
f
f
Combination of true/false that describes
the order of RED, GREEN, ORANGE
D Goforth - COSC 4117, fall 2006
8
Logical equivalences
Review the truth tables for each of these connectives:





Practice applying these logical equivalence axioms
Uses of logical equivalence axioms
 Rewriting sentences
 Show equivalence or difference
 Format for reasoning
 Reduce number of connectives
(people like variety; computers like simplicity)
e.g.,
A  B ( A  B )  ( B  A )
 ( A  B )  ( B  A )
 (A  B )  (B  A )
D Goforth - COSC 4117, fall 2006
11
Properties of sentences
 validity: sentence is true in all models
 satisfiability: sentence is true in some
model
• general knowledge is valid;
• facts are (should be) satisfiable
D Goforth - COSC 4117, fall 2006
12
Proof strategies
A. finding models that satisfy KB
– truth table enumeration O(2n) for
n propositions
B. applying inference rules
D Goforth - COSC 4117, fall 2006
13
B. Inference rules
 human-like reasoning from classic logic
1. and elimination
2. modus ponens
3. logical equivalences
D Goforth - COSC 4117, fall 2006
14
1. And elimination
 Spot is big and friendly
 Spot is friendly
 AΛB
B
D Goforth - COSC 4117, fall 2006
15
2. Modus ponens
 Spot is a dog
A dog is a mammal
(if Spot is a dog then Spot is a mammal)
 Spot is a mammal
 A , A=>B
B
D Goforth - COSC 4117, fall 2006
16
3. Logical equivalence (eg)
 logical equivalence:
 ~(A
\/
B ) = ~A Λ ~B
 The car is not (red or green)
 The car is not red
and it’s not green
 ~ ( A \/ B )
~A Λ ~B
 Question – can we claim “car is not red”?
D Goforth - COSC 4117, fall 2006
17
Short inference sequence
Propositions: A car is red
B car is green
Knowledge: ~ ( A \/ B )
Inference:
~ ( A \/ B )
~A Λ ~B
(logical equivalence)
~A
(and elimination)
Claim: car is not red
D Goforth - COSC 4117, fall 2006
18
Automated reasoning
 reduced variety of representation for
sentences
 harder to ‘read’ for humans
 simpler data structure to process
 reduced set of inference rules
 less efficient for humans
 equally powerful
 simpler algorithm for implication
D Goforth - COSC 4117, fall 2006
19
Simplified representation - CNF
Conjunctive Normal Form
 conjunction of disjunctions (AND of OR’s)
of literals (atomic propositions or negations)
 (P \/ Q \/ ~R) Λ (~W \/ ~Q \/ T) Λ (W \/ P)
 A Knowledge base is in CNF if the
statements are disjunctions
D Goforth - COSC 4117, fall 2006
20
Example sentence
Example sentence in CNF
less readable?
Restricted CNF – Horn clause
CNF disjunction
 At most one literal is positive
 (P \/ Q \/ ~R) is not Horn clause
 (~W \/ ~Q \/ T) is Horn clause
 Basis of PROLOG – logic programming
language
 (~W \/ ~Q \/ T) is (W Λ Q)  T
D Goforth - COSC 4117, fall 2006
22
Summary 1
 Representation – facts, propositions,
general knowledge
 Models, validity and satisfiability
 Propositional logic
 Reasoning – by searching models
– by inference
 CNF, Horn clauses
D Goforth - COSC 4117, fall 2006
23
Summary 2
 Logical equivalence axioms
 Sound and complete inference
 Inference strategies
 And elimination
 Modus ponens
 Resolution
 Inference algorithms (coming next)
 Resolution proof by contradiction
 Forward chaining – data-driven
 Backward chaining –goal-directed
D Goforth - COSC 4117, fall 2006
24