CPSC 312 — Functional and Logic Programming
Assignment 4 is due Thursday!
“Logic is the beginning of wisdom, not the end.”
Leonard Nimoy “Star Trek VI: The Undiscovered Country” 1991
CPSC 312 — Lecture 20 1 / 27
©D. Poole 2021
Plan
Done:
Syntax and semantics of propositional definite clauses Model a simple domain using propositional definite clauses
Today:
Soundness and completeness of a proof procedure Bottom-up proof procedure
Bottom-up proof procedure: soundness and completeness Top-down proof procedure
Procedural definition (box model)
CPSC 312 — Lecture 20 2 / 27
©D. Poole 2021
Semantics
An interpretation I assigns a truth value to each atom. rule h :- b1,…,bk is true unless
h is false and b1 …bk are all true.
A model of a set of clauses is an interpretation in which all
the clauses (atomic facts and rules) 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.
CPSC 312 — Lecture 20 3 / 27
©D. Poole 2021
Proofs
A proof is a mechanically derivable demonstration that a formula logically follows from 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.
If a sound proof procedure produces a result, the result is correct.
A proof procedure is complete if KB |= g implies KB ⊢ g. A complete proof procedure can produce all results.
CPSC 312 — Lecture 20 4 / 27
©D. Poole 2021
Clicker Question
Suppose there at some atom aaa such that KB ⊢ aaa and
KB ̸|= aaa.
What can be inferred?
A The proof procedure is not sound
B The proof prodecure is not complete
C The proof procedure is sound and complete
D The proof procedure is either sound or complete E None of the above
©D. Poole 2021
CPSC 312 — Lecture 20 5 / 27
Bottom-up Proof Procedure
One 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.
(An atomic fact is treated as a clause with empty body (m = 0).)
©D. Poole 2021
CPSC 312 — Lecture 20 6 / 27
Bottom-up proof procedure
KB ⊢ g if g ∈ C at the end of this procedure:
C := {}; repeat
select fact h or a rule“h :- b1, …, bm” in KB such that bi ∈ C for all i, and
h ∈/ C ; until no more clauses can be selected.
C := C ∪ {h}
©D. Poole 2021
CPSC 312 — Lecture 20 7 / 27
Example (simpeg.pl)
a :- b, c.
a :- e, f.
b :- f, k.
c :- e.
d :- k.
e.
f :- j, e.
f :- c.
j :- c.
©D. Poole 2021
CPSC 312 — Lecture 20 8 / 27
Clicker Question
Consider the knowledge base KB:
aah :- green. ahh :- blue. green.
xox :- bar, fun. bar :- zed.
zed .
What is the final consequence set in the bottom-up proof procedure run on KB?
A {aah,blue,green,xox,bar,fun,zed} B {aah,blue,green,xox,bar,zed}
C {aah,green,bar,zed}
D {green,bar,zed}
E None of the above
©D. Poole 2021
CPSC 312 — Lecture 20 9 / 27
Soundness of bottom-up proof procedure
IfKB⊢g thenKB|=g.
Supposethereisag suchthatKB⊢g andKB̸|=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.
h was added to C, so there must be a clause in KB h:-b1, …,bm
whereeachbi isinC,andsotrueinI. h is false in I (by assumption)
So this clause is false in I.
Therefore I isn’t a model of KB.
Contradiction. Therefore there cannot be such a g. CPSC 312 — Lecture 20
10 / 27
©D. Poole 2021
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.
Claim: 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.
CPSC 312 — Lecture 20
11 / 27
©D. Poole 2021
Completeness
IfKB|=g thenKB⊢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.
CPSC 312 — Lecture 20 12 / 27
©D. Poole 2021
Clicker Question
Consider the knowledge base KB:
aah :- blue. aah :- green. green.
xox :- bar, fun. bar :- zed.
zed .
What is the set of atoms that are true in the minimal model of KB?
A {aah,blue,green,xox,bar,fun,zed} B {aah,blue,green,xox,bar,zed}
C {aah,green,bar,zed}
D {green,bar,zed}
E None of the above
©D. Poole 2021
CPSC 312 — Lecture 20 13 / 27
Top-down Definite Clause 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 a1 with the clause in the knowledge base:
a1 :- b1, …, bp is the answer clause
yes :- b1, ···, bp, a2, ···, am.
A fact in the knowledge base is considered as a clause where p = 0.
CPSC 312 — Lecture 20 14 / 27
©D. Poole 2021
Example (simpeg.pl)
a :- b, c.
a :- e, f.
b :- f, k.
c :- e.
d :- k.
e.
f :- j, e.
f :- c.
j :- c.
©D. Poole 2021
CPSC 312 — Lecture 20 15 / 27
Clicker Question
Given the answer clause
yes :- good, happy, green.
Which clause in a KB could this be resolved with (i) green :- good.
(ii) good.
(iii) happy :- green.
(iv) good :- nice, green.
(v) happy, green Click on:
A (i), (ii) and (iv) only B (ii) and (iv) only
C (ii) only
D (iii) and (v) only
E none of the above
©D. Poole 2021
CPSC 312 — Lecture 20 16 / 27
Clicker Question
Given the answer clause
yes :- good, happy, green.
What is the result of resolving this with the clause
good :- nice, green.
A yes :- good, nice, green, happy, green B good :- happy, green
C yes :- happy, green
D yes :- nice, green, happy, green
E yes :- nice, green, good, happy, green
©D. Poole 2021
CPSC 312 — Lecture 20 17 / 27
Clicker Question
Given the answer clause
yes :- happy, green, good.
What is the result of resolving this with the clause
happy .
A yes :- good, nice, green, happy, green B happy :- green, good
C yes :- happy, green
D yes :- happy, green, good
E yes :- green, good
©D. Poole 2021
CPSC 312 — Lecture 20 18 / 27
Derivations
An answer is an answer clause with m = 0. That is, it is the answer clause yes :- .
A derivation of query “?q1, . . . , qk ” from KB is a sequence ofanswerclausesγ0,γ1,…,γn suchthat
γ0 is the answer clause yes :- q1, …, qk γi the resolution of γi−1 with a clause in KB γn is an answer.
CPSC 312 — Lecture 20 19 / 27
©D. Poole 2021
Top-down definite clause interpreter
To solve the query ?q1, …, qk:
ac:=“yes:-q1, …,qk” repeat
select leftmost atom a1 from the body of ac choose clause C from KB with a1 as head replace a1 in the body of ac by the body of C
until ac is an answer.
©D. Poole 2021
CPSC 312 — Lecture 20 20 / 27
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”
CPSC 312 — Lecture 20 21 / 27
©D. Poole 2021
Example: successful derivation
a:-b, c. c :- e.
f :- j, e.
Query: ?a
γ0: yes:-a γ1: yes:-e,f γ2: yes:-f γ3: yes:-c
a:-e, f. d :- k.
f :- c.
b:-f, k. e.
j :- c.
γ4: yes:-e γ5: yes:-
©D. Poole 2021
CPSC 312 — Lecture 20 22 / 27
Example: failing derivation
a:-b, c. c :- e.
f :- j, e.
Query: ?a
a:-e, f. d :- k.
f :- c.
b:-f, k. e.
j :- c.
γ4: yes:-e,k,c γ5: yes:-k,c
γ0: yes:-a
γ1: yes:-b,c γ2: yes:-f,k,c γ3: yes:-c,k,c
©D. Poole 2021
CPSC 312 — Lecture 20 23 / 27
Search Graph for SLD Resolution
yes :- a, d yes:-b, c, d yes:-g, d
yes:-j, c, d yes:-m, d yes:-k, c, d
yes:-h, d yes:-m, d
yes:- f, d yes:-p, d
yes :- d yes:-m yes:-p
yes :-
1
a:-b, a:-h. b:-k. d:-p. f:-p. g:-f. h :- m. ?a, d.
c.
a:-g. yes:-m, c, d b:-j.
d:-m.
f:-m.
g:-m. k:-m. p.
yes:-m, d
©D. Poole 2021
CPSC 312 — Lecture 20 24 / 27
Clicker Question
Given the answer clause
yes :- good, happy, green.
Which clause in a KB could this be resolved with (i) green :- good.
(ii) good.
(iii) happy :- green.
(iv) good :- nice, green.
(v) happy, green Click on:
A (i), (ii) and (iv) only B (ii) and (iv) only
C (ii) only
D (iii) and (v) only
E none of the above
©D. Poole 2021
CPSC 312 — Lecture 20 25 / 27
Clicker Question
Given the answer clause
yes :- good, happy, green.
What is the result of resolving this with the clause
good :- nice, green.
A yes :- good, nice, green, happy, green B good :- happy, green
C yes :- happy, green
D yes :- nice, green, happy, green
E none of the above
©D. Poole 2021
CPSC 312 — Lecture 20 26 / 27
Soundness and completeness of top-down proof procedure
Is top-down proof procedure with depth-first search sound?
Yes!
Is top-down proof procedure with depth-first search complete?
No!
a :- b. b :- a. b :- c. c.
?a.
This can get stuck in an infinite loop.
CPSC 312 — Lecture 20
27 / 27
©D. Poole 2021