52KRproplogicegs
Download
Report
Transcript 52KRproplogicegs
Reasoning Algorithms
in Propositional Logic
Examination will be a take-home exam;
confirmation coming as soon as signed course
evaluation is received in registrar’s office
Knowledge representation
and reasoning
Propositions, general knowledge, facts,
KB, model
-> big truth table
Propositions
KB: general knowledge & facts
ttftftffft
ttttttttttttttttttttttttttt
model
The reasoning problems:
1. Find t/f assignment(s) model(s) where KB is true
2. Answering questions “entailed” by KB
D Goforth - COSC 4117, fall 2006
2
Approaches to reasoning
N propositions to satisfy KB
1. Search through 2N rows of truth table:
goal-based search, fitness is truth of KB
(SAT)
2. Use inference: restrict attention to
relevant propositions (assumes many
models satisfy the KB and many
propositions might be “don’t care”)
D Goforth - COSC 4117, fall 2006
3
Approaches to Reasoning:
strategies
1. Search
a) Depth-first exhaustive search from start
state of ‘empty’ truth table
b) Hill-climbing from random start state of
true-false assignments
2. Inference
a) Forward chaining from KB to query
b) Backward chaining from query into KB
D Goforth - COSC 4117, fall 2006
4
Propositional satisfiability Problem
(SAT)
Definition (Hoos & Stutzle, 2005)
“Given a propositional formula F, the
problem is to decide whether or not F is
satisfiable.”
F = KB (facts + general knowledge)
D Goforth - COSC 4117, fall 2006
5
Propositional satisfiability Problem
(SAT)
State: a vector of truth values for the n
propositions
State space: 2n nodes
Goal state(s): KB is true (a model)
e.g., n = 5, {P1,P2,P3,P4,P5}
1 b)
ttftf
t-f
ftftf
t-f
ttttf
etc.
KB = (P1P2) (P2P1)
(P1 P2 P3)
(P2P1) (P4P3)
(P5P3)
D Goforth - COSC 4117, fall 2006
6
Propositional satisfiability Problem
(SAT)
TT-ENTAILS is depth-first search, exhaustive,
incremental
Improvement in efficiency by pruning: DPLL –
p.221
early termination
pure symbol heuristic
unit clause heuristic
WALKSAT: complete state algorithm – reduce
number of false clauses by flipping propositions
true<->false
D Goforth - COSC 4117, fall 2006
7
Propositional satisfiability Problem
(SAT)
Answers a question: Is a sentence a true in the KB?
i.e., is the sentence true in all models of the KB which
are true? OR is (KBa) true?
Question: (P1P5) ?
1 a)
tt
KB = (P1P2) (P2P1)
f
ttf
t
ttt
etc.
(P1 P2 P3)
(P2P1) (P4P3)
(P5P3)
D Goforth - COSC 4117, fall 2006
8
1 a)
at root – no truth
values assigned
KB,
α both true?
KB false
P both true and false
Question: (P1P5) ?
KB = (P1P2) (P2P1)
f
tt
t
(P1 P2 P3)
ttf
(P2P1) (P4P3)
etc.
ttt
(P5P3)
TT-ENTAILS
1 a)
Propositions
KB
KB Q
Question
P1 P2 P3 P4 P5 (P1P2)(P2P1)(P1P2P3)(P2P1)(P4P3)(P5 (P1P5)
P3)
t
t t t t t
t
t
f
t
t
t
t
t
t
t
f
t
t
…
f
f
f
f
f
t
f
…
t
t
…
t
t
t
t
t
t
t
t
f
t
…
f
TT-ENTAILS returns true if KB Q is true for all cases;
i.e., there is no row with KB true and Q false
Variations on TT-ENTAILS
For efficiency: (see p.221)
Early termination (pruning)
Pure symbol heuristic
Unit clause heuristic
D Goforth - COSC 4117, fall 2006
11
Propositional satisfiability Problem
(SAT)
WALKSAT, p.223 (complete state search)
Checks satisfiability
i.e., are there models of the KB which are true?
Question: KB satisfiable?
1 b)
t-f
ttftf
ftftf
t-f
ttttf
etc.
KB = (P1P2) (P2P1)
(P1 P2 P3)
(P2P1) (P4P3)
(P5P3)
D Goforth - COSC 4117, fall 2006
12
1 b)
Question: KB satisfiable?
1 b)
ttftf
t-f
ttttf
t-f
KB = (P1P2) (P2P1)
(P1 P2 P3)
ftftf
(P2P1) (P4P3)
etc.
(P5P3)
WALKSAT
random
ftftf
Satisfied?
Give up?
y
y
true
false
pick random false clause
Probability p
flip t/f of random
proposition in clause
flip t/f of proposition
in clause that
minimizes number of
false clauses
WALKSAT performance
Not guaranteed to find solution
(not exhaustive like TT-ENTAILS)
More effective in practice than
TT-ENTAILS, even with efficiency
heuristics (DPLL)
1 b)
D Goforth - COSC 4117, fall 2006
15
Approaches to reasoning
N propositions to satisfy KB
1. Search through 2N rows of truth table:
goal-based search, fitness is truth of KB
(SAT)
2. Use inference: restrict attention to
relevant propositions (assumes many
models satisfy the KB and many
propositions might be “don’t care”)
D Goforth - COSC 4117, fall 2006
16
Inference rule: Resolution
elimination of complementary literals
from sentences in CNF
Part of KB
(~W \/ ~Q \/ T) Λ (W \/ P)
(~Q \/ T \/ P)
New proposition
inference by resolution is
Sound – only infers true statements
Complete – anything entailed is derivable
D Goforth - COSC 4117, fall 2006
17
Resolution: Example
(P11 \/ P22 \/ P13)
Part of KB
~P11
~P22
resolve (P11 \/ P22 \/ P13), ~P11
(P22 \/ P13)
resolve (P22 \/ P13), ~P22
P13
(from Wumpus world)
D Goforth - COSC 4117, fall 2006
18
Resolution algorithm
goal-directed proof by contradiction
to prove P
assume ~P
add ~P to KB
resolve in KB till resulting sentence is
1. in KB (therefore P is false)
2. empty (therefore ~P is contradictory so P is
true)
D Goforth - COSC 4117, fall 2006
19
α leads to
contradition
Figure 7.12
p.216
α is consistent
therefore
with KB so
α is true
α is false
2 a)
Horn clause inference method
compromise representation that is
human-readable
basic of logic programming (Prolog)
uses modus ponens, not resolution
like CNF but restricted to only one
positive proposition
(~W \/ ~Q \/ ~S \/ T)
=>
~(W Λ Q Λ S) \/ T
=>
(W Λ Q Λ S) T
D Goforth - COSC 4117, fall 2006
21
2 a)
Forward chaining inference with
Horn clauses
algorithm to determine if a particular
proposition is true
O(n) in size of KB!!
p. 219, Fig 7.14
D Goforth - COSC 4117, fall 2006
22
Reasoning by
FORWARD chaining
Figure 7.14
p.219
2 a)
•From the known data
“forward” to unknown
•Doesn’t need goal –
self-directed agent
2 b)
Reasoning by BACKWARD chaining
Goal-directed reasoning – question
answering agent
Backward (KB, Q) //answer query Q
If Q true in KB, return true
For each Horn clause (P=>Q) in KB,
If Backward (KB, P), return true
Return false
D Goforth - COSC 4117, fall 2006
24