CPSC 312 — Functional and Logic Programming
Assignment 4 is due next Thursday!
“Consequently he who wishes to attain to human perfection, must therefore first study Logic, next the various branches of Mathematics in their proper order, then Physics, and lastly Metaphysics.”
Maimonides 1135–1204
CPSC 312 — Lecture 19 1 / 22
©D. Poole 2021
Plan
Logic Programming
Propositional logic programs Semantics
Bottom-up and top-down proof procedures Datalog
Logic programs with function symbols
Applications (e.g., natural language processing) Semantic web
Today:
Syntax and semantics of propositional definite clauses
Model a simple domain using propositional definite clauses Bottom-up proof procedure
CPSC 312 — Lecture 19 2 / 22
©D. Poole 2021
Datalog Syntax
An atom is of the form p(t1,…,tn) or p
p is a predicate symbol, starts with lower-case letter each ti is a term which is either:
a constant: a number or a word starting with a lower-case letter
a logical variable: a word starting with an upper-case letter A definite clause is either
an atomic clause: atom. or
a rule: h :- b1,…,bk. where h and each bi is an atom.
:- means “if”
, means “and”
the rule is read “h is true if b1 and … and bk”
A logic program or knowledge base is a set of definite clauses A query is of the form b1,…bk. where each bi is an atom. comments start with % to end of line
CPSC 312 — Lecture 19 3 / 22
©D. Poole 2021
Human’s view of semantics
Step 1 Step 2
Step 3
Step 4
Begin with a task domain.
Choose atoms in the computer to denote propositions. These atoms have meaning to the KB designer.
Tell the system knowledge about the domain.
Ask the system questions.
— The system gives answers.
— Person can interpret the answer with the meaning associated with the atoms.
©D. Poole 2021
CPSC 312 — Lecture 19 4 / 22
Electrical Environment (see elect prop.pl)
cb1
w5
outside power
circuit breaker
off
on switch
two-way switch
light
power outlet
s1
cb2
s2 w1 w2
s3
w3
w6
p2
p1
w0
w4
l1
l2
©D. Poole 2021
CPSC 312 — Lecture 19 5 / 22
Role of semantics in electrical environment
In user’s mind:
light1 broken: light 1 is broken
sw1 up: switch 1 is up sw2 up: switch 2 is up
power: there is power in the building
unlit light1: light 1 isn’t lit
lit light2: light 2 is lit
The computer doesn’t know the meaning of the symbols
The user can interpret the symbol using their meaning
In computer:
light1 broken :- sw1 up,
sw2 up, power, unlit light1.
sw1 up.
sw2 up.
power :- lit light2. unlit light1.
lit light2.
Conclusion: light1 broken
CPSC 312 — Lecture 19 6 / 22
©D. Poole 2021
A progression of logical languages
Propositional logic programs: atoms only have constants as arguments (no variables).
Datalog: allow for logical variables in clauses. Pure Prolog: Datalog + function symbols
CPSC 312 — Lecture 19 7 / 22
©D. Poole 2021
Semantics
An interpretation I assigns a truth value to each atom. True of compound propositions in interpretation is derived
from truth table:
p qp,qp:-q true true true true true false false true
false true false false false false false true
Abody(b1, b2)istrueinI ifb1 istrueinI andb2 istrueinI. Aruleh:-bisfalseinI ifbistrueinI andhisfalseinI.
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.
CPSC 312 — Lecture 19 8 / 22
©D. Poole 2021
Models and Logical Consequence
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 19 9 / 22
©D. Poole 2021
Simple Example (clicker question)
I1 I2 I3 I4 I5
true true false false true true true true true true
true false false true false
true false false false true
p :- q. KB = q.
r :- s. pqrs
A yes
B no
C I’m not sure
model of KB? isamodelofKB not a model of KB isamodelofKB isamodelofKB not a model of KB
Does q, p, r , s logically follow from KB? KB |= q, KB |= p, KB ̸|= r, KB ̸|= s
©D. Poole 2021
CPSC 312 — Lecture 19 10 / 22
Clicker Question
Consider the knowledge base KB:
happy :- good. happy :- green. green.
foo :- bar, fun. bar :- zed.
zed .
Which of the following are true ( KB ̸|= g means “g is a not a
logical consequence of KB”) KB |= foo
KB ̸|= foo
KB |= foo
A KB |= happy and
B KB |= happy and
C KB ̸|= happy and
D KB ̸|= happy and
E I’m not sure, please explain it again.
KB ̸|= foo
©D. Poole 2021
CPSC 312 — Lecture 19 11 / 22
Clicker Question
Consider the knowledge base KB:
happy :- good. happy :- green. green.
foo :- bar, fun. bar :- zed.
zed .
What is the set of all atoms that are logical consequences of KB?
A {happy,good,green,foo,bar,fun,zed} B {happy,good,green,foo,bar,zed}
C {happy,green,bar,zed}
D {green,bar,zed}
E None of the above
©D. Poole 2021
CPSC 312 — Lecture 19 12 / 22
User’s view of Semantics
1. Choose a task domain: intended interpretation.
2. Associate an atom with each proposition you want to
represent.
3. Tell the system clauses that are true in the intended
interpretation: axiomatizing the domain.
4. Ask questions about the intended interpretation.
5. If KB |= g, then g must be true in the intended interpretation.
6. Users can interpret the answer using their intended interpretation of the symbols.
©D. Poole 2021
CPSC 312 — Lecture 19 13 / 22
Computer’s view of semantics
The computer doesn’t have access to the intended interpretation.
All it knows is the knowledge base.
The computer can determine if a formula is a logical consequence of KB.
If KB |= g then g must be true in the intended interpretation. If KB ̸|= g then there is a model of KB in which g is false.
This could be the intended interpretation.
CPSC 312 — Lecture 19 14 / 22
©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 19 15 / 22
©D. Poole 2021
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 19 16 / 22
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 19 17 / 22
Example
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 19 18 / 22
Clicker Question
Consider the knowledge base KB:
happy :- good. happy :- green. green.
foo :- bar, fun. bar :- zed.
zed .
What is the final consequence set in the bottom-up proof procedure run on KB?
A {happy,good,green,foo,bar,fun,zed} B {happy,good,green,foo,bar,zed}
C {happy,green,bar,zed}
D {green,bar,zed}
E None of the above
©D. Poole 2021
CPSC 312 — Lecture 19 19 / 22
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 19
20 / 22
©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 19
21 / 22
©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 19 22 / 22
©D. Poole 2021