Propositions and inference
Propositions and inference
Chapter 5
David Poole and Alan Mackworth
Chapter 5 Propositions and inference 1 / 22
Electrical Environment
light
two-way
switch
switch
off
on
power
outlet
circuit breaker
outside power
cb1
s1
w1
s2 w2
w0
l1
w3
s3
w4
l2
p1
w5
cb2
w6
p2
Chapter 5 Propositions and inference 2 / 22
Representing the Electrical Environment
light l1.
light l2.
down s1.
up s2.
up s3.
ok l1.
ok l2.
ok cb1.
ok cb2.
live outside.
lit l1 ← live w0 ∧ ok l1
live w0 ← live w1 ∧ up s2.
live w0 ← live w2 ∧ down s2.
live w1 ← live w3 ∧ up s1.
live w2 ← live w3 ∧ down s1.
lit l2 ← live w4 ∧ ok l2.
live w4 ← live w3 ∧ up s3.
live p1 ← live w3.
live w3 ← live w5 ∧ ok cb1.
live p2 ← live w6.
live w6 ← live w5 ∧ ok cb2.
live w5 ← live outside.
Chapter 5 Propositions and inference 3 / 22
Role of semantics
In computer:
light1 broken← sw up
∧ power ∧ unlit light1.
sw up.
power ← lit light2.
unlit light1.
lit light2.
In user’s mind:
light1 broken: light #1
is broken
sw up: switch is up
power : there is power in
the building
unlit light1: light #1
isn’t lit
lit light2: light #2 is lit
Conclusion: light1 broken
The computer doesn’t know the meaning of the symbols
The user can interpret the symbol using their meaning
Chapter 5 Propositions and inference 4 / 22
Simple language: propositional definite clauses
An atom is a symbol starting with a lower case letter
A body is an atom or is of the form b1 ∧ b2 where b1 and b2
are bodies.
A definite clause is an atom or is a rule of the form h← b
where h is an atom and b is a body.
A knowledge base is a set of definite clauses
Chapter 5 Propositions and inference 5 / 22
Semantics
An interpretation I assigns a truth value to each atom.
A body b1 ∧ b2 is true in I if b1 is true in I and b2 is true in I .
A rule h← b is false in I if b is true in I and h is false in I .
The rule is true otherwise.
A knowledge base KB is true in I if and only if every clause in
KB is true in I .
Chapter 5 Propositions and inference 6 / 22
Models and Logical Consequence
A model of a set of clauses is an interpretation in which all
the clauses are true.
If KB is a set of clauses and g is a conjunction of atoms, g is
a logical consequence of KB, written KB |= g , if g is true
in every model of KB.
That is, KB |= g if there is no interpretation in which KB is
true and g is false.
Chapter 5 Propositions and inference 7 / 22
Simple Example
KB =
p ← q.
q.
r ← s.
How many interpretations?
p q r s model of KB?
I1 true true true true
yes
I2 false false false false
no
I3 true true false false
yes
I4 true true true false
yes
I5 true true false true
no
Which of p, q, r , s logically follow from KB?
KB |= p, KB |= q, KB 6|= r , KB 6|= s
Chapter 5 Propositions and inference 8 / 22
Simple Example
KB =
p ← q.
q.
r ← s.
How many interpretations?
p q r s model of KB?
I1 true true true true yes
I2 false false false false no
I3 true true false false yes
I4 true true true false yes
I5 true true false true no
Which of p, q, r , s logically follow from KB?
KB |= p, KB |= q, KB 6|= r , KB 6|= s
Chapter 5 Propositions and inference 8 / 22
Proof procedures
A proof procedure is a – possibly non-deterministic –
algorithm for deriving consequences of a knowledge base.
Given a proof procedure, KB ` g means g can be derived
from knowledge base KB.
Recall KB |= g means g is true in all models of KB.
A proof procedure is sound if KB ` g implies KB |= g .
A proof procedure is complete if KB |= g implies KB ` g .
Chapter 5 Propositions and inference 9 / 22
Bottom-up proof procedure
Rule of derivation (a generalized form of modus ponens):
If “h ← b1 ∧ . . . ∧ bm” is a clause in the knowledge base,
and each bi has been derived, then h can be derived.
This is forward chaining on this clause.
(This rule also covers the case when m = 0.)
Chapter 5 Propositions and inference 10 / 22
Bottom-up proof procedure
KB ` g if g ∈ C at the end of this procedure:
C := {};
repeat
select clause “h← b1 ∧ . . . ∧ bm” in KB such that
bi ∈ C for all i , and
h /∈ C ;
C := C ∪ {h}
until no more clauses can be selected.
Chapter 5 Propositions and inference 11 / 22
Example
a← b ∧ c .
a← e ∧ f .
b ← f ∧ k.
c ← e.
d ← k .
e.
f ← j ∧ e.
f ← c.
j ← c .
Chapter 5 Propositions and inference 12 / 22
Soundness of bottom-up proof procedure
If KB ` g then KB |= g .
Suppose there is a g such that KB ` g and KB 6|= g .
Then there must be a first atom added to C that isn’t true in
every model of KB. Call it h. Suppose h isn’t true in model I
of KB.
There must be a clause in KB of form
h← b1 ∧ . . . ∧ bm
Each bi is true in I . h is false in I . So this clause is false in I .
Therefore I isn’t a model of KB.
Contradiction.
Chapter 5 Propositions and inference 13 / 22
Fixed Point
The C generated at the end of the bottom-up algorithm is
called a fixed point.
Let I be the interpretation in which every element of the fixed
point is true and every other atom is false.
I is a model of KB.
Proof: suppose h← b1 ∧ . . . ∧ bm in KB is false in I . Then h
is false and each bi is true in I . Thus h can be added to C .
Contradiction to C being the fixed point.
I is called a Minimal Model.
Chapter 5 Propositions and inference 14 / 22
Completeness of bottom-up proof procedure
If KB |= g then KB ` g .
Suppose KB |= g . Then g is true in all models of KB.
Thus g is true in the minimal model.
Thus g is in the fixed point.
Thus g is generated by the bottom up algorithm.
Thus KB ` g .
Chapter 5 Propositions and inference 15 / 22
Top-down proof procedure
Idea: search backward from a query to determine if it is a logical
consequence of KB.
An answer clause is of the form:
yes ← a1 ∧ a2 ∧ . . . ∧ am
The SLD Resolution of this answer clause on atom ai with the
clause:
ai ← b1 ∧ . . . ∧ bp
is the answer clause
yes ← a1∧. . .∧ai−1 ∧ b1∧ · · · ∧bp ∧ ai+1∧ · · · ∧am.
An answer is an answer clause with m = 0. That is, it is the
answer clause yes ← .
Chapter 5 Propositions and inference 16 / 22
Derivations
A derivation of query “?q1 ∧ . . . ∧ qk” from KB is a sequence of
answer clauses γ0, γ1, . . . , γn such that
γ0 is the answer clause yes ← q1 ∧ . . . ∧ qk ,
γi is obtained by resolving γi−1 with a clause in KB, and
γn is an answer.
Chapter 5 Propositions and inference 17 / 22
Top-down proof procedure
To solve the query ?q1 ∧ . . . ∧ qk :
ac := “yes ← q1 ∧ . . . ∧ qk”
repeat
select atom ai from the body of ac
choose clause C from KB with ai as head
replace ai in the body of ac by the body of C
until ac is an answer.
Chapter 5 Propositions and inference 18 / 22
Nondeterministic Choice
Don’t-care nondeterminism If one selection doesn’t lead to a
solution, there is no point trying other alternatives. select
Don’t-know nondeterminism If one choice doesn’t lead to a
solution, other choices may. choose
Chapter 5 Propositions and inference 19 / 22
Example: successful derivation
a← b ∧ c . a← e ∧ f . b ← f ∧ k .
c ← e. d ← k . e.
f ← j ∧ e. f ← c . j ← c.
Query: ?a
γ0 : yes ← a γ4 : yes ← e
γ1 : yes ← e ∧ f γ5 : yes ←
γ2 : yes ← f
γ3 : yes ← c
Chapter 5 Propositions and inference 20 / 22
Example: failing derivation
a← b ∧ c . a← e ∧ f . b ← f ∧ k .
c ← e. d ← k . e.
f ← j ∧ e. f ← c . j ← c.
Query: ?a
γ0 : yes ← a γ4 : yes ← e ∧ k ∧ c
γ1 : yes ← b ∧ c γ5 : yes ← k ∧ c
γ2 : yes ← f ∧ k ∧ c
γ3 : yes ← c ∧ k ∧ c
Chapter 5 Propositions and inference 21 / 22
Search Graph for SLD Resolution
a← b ∧ c . a← g .
a← h. b ← j .
b ← k . d ← m.
d ← p. f ← m.
f ← p. g ← m.
g ← f . k ← m.
h← m. p.
?a ∧ d
yes←a^d
yes←j^c^d
yes←k^c^d
yes←m^c^d
yes←g^dyes←b^c^d
yes←m^d
yes←m^d
yes←f^d
yes←p^d
yes←d
yes←m yes←p
yes←h^d
yes←m^d
yes←
Chapter 5 Propositions and inference 22 / 22