CS计算机代考程序代写 chain AI algorithm Propositions and inference

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