Announcements
Last Class!
For more details about the exam and possibly a review session (do you want one?) — see schedule tab and Piazza.
What is now required is to give the greatest possible de- velopment to mathematical logic, to allow to the full the importance of relations… If this can be successfully ac- complished, there is every reason to hope that the near future will be as great an epoch in pure philosophy as the immediate past has been in the principles of mathematics. Great triumphs inspire great hopes; and pure thought may achieve, within our generation, such results as will place our time, in this respect, on a level with the greatest age of Greece.
– Bertrand Russell, Mysticism and Logic and Other Essays [1917]
CPSC 312 — Lecture 33 1 / 19
©D. Poole 2021
Since Last midterm
difference lists, definite clause grammars and natural language interfaces to databases
computer algebra and calculus
Triples are universal representations of relations, and are the basis for RDF, and knowledge graphs
URIs provide constants that have standard meanings
Ontologies define the meaning of symbols used in information systems.
You should know what the following mean: RDF, URI, rdf:type, rdfs:subClassOf, rdfs:domain, rdfs:range
Complete knowledge assumption and negation as failure
Substitutions and Unification Today
Proofs and answers. Negation with variables.
CPSC 312 — Lecture 33 2 / 19
©D. Poole 2021
Unifiers
Substitution σ is a unifier of e1 and e2 if e1σ = e2σ. Substitution σ is a most general unifier (mgu) of e1 and e2 if
σisaunifierofe1 ande2;and
if substitution σ′ also unifies e1 and e2, then eσ′ is an instance
of eσ for all atoms e.
If two atoms have a unifier, they have a most general unifier.
If there are more than one most general unifiers, they only differ in the names of the variables.
CPSC 312 — Lecture 33 3 / 19
©D. Poole 2021
Top-down propositional definite clause interpreter (review)
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 33 4 / 19
Top-down Proof procedure
A generalized answer clause is of the form yes(t1,…,tk) :- a1, a2, …, am,
where t1,…,tk are terms and a1,…,am are atoms.
The SLD resolution of this generalized answer clause on a1
with the clause
a:-b1, …,bp,
where ai and a have most general unifier θ, is
(yes(t1,…,tk) :- b1, …, bp, a2, …, am)θ.
CPSC 312 — Lecture 33 5 / 19
©D. Poole 2021
Top-down Proof Procedure
To solve query ?B with variables V1, . . . , Vk :
Set ac to generalized answer clause yes(V1, . . . , Vk ) :- B while body of ac is not empty do
Suppose ac is yes(t1,…,tk) :- a1, a2, …, am select leftmost atom a1 in the body of ac choose clause a :- b1, …, bp in KB
Rename all variables in a :- b1, …, bp
Let θ be the most general unifier of ai and a. Fail if they don’t unify
Set ac to (yes(t1,…,tk) :- b1, …, bp, a2, …, am)θ end while
Suppose ac is generalized answer clause yes(t1, . . . , tk ) :- Answer is V1 = t1,…,Vk = tk
©D. Poole 2021
CPSC 312 — Lecture 33 6 / 19
Example
live(Y) :- connected to(Y,Z), live(Z). live (outside ).
connected to(w6, w5).
connected to(w5, outside).
? live(A).
yes(A) :- live(A).
yes(A) :- connected to(A, Z1), live(Z1). yes(w6) :- live(w5).
yes(w6) :- connected to(w5, Z2), live(Z2). yes(w6) :- live(outside).
yes(w6) :- .
Answer is A = w6
©D. Poole 2021
CPSC 312 — Lecture 33 7 / 19
Example
append ([], L, L).
append([H | T],A,[H | R]) :-
append(T,A,R).
? append([a, b, c], [1, 2, 3], L).
yes(L) :- append([a, b, c], [1, 2, 3], L).
yes([a | R1]) :- append([b, c], [1, 2, 3], R1). yes([a, b | R2]) :- append([c], [1, 2, 3], R2). yes([a, b, c | R3]) :- append([], [1, 2, 3], R3). yes([a,b,c,1,2,3]) :- .
Answer is L = [a,b,c,1,2,3]
©D. Poole 2021
CPSC 312 — Lecture 33 8 / 19
Example
elem(E, set(E,_,_)).
elem(V, set(E,LT,_)) :-
V #< E,
elem(V,LT).
elem(V, set(E,_,RT)) :-
E #< V,
elem(V,RT).
?- elem(3,S),elem(8,S).
yes(S) :- elem(3,S),elem(8,S)
yes(set(3,S1,S2)) :- elem(8, set(3,S1,S2))
yes(set(3,S1,S2)) :- 3 #< 8, elem(8,S2)
yes(set(3,S1,S2)) :- elem(8,S2)
yes(set(3,S1,set(8,S3,S4))) :-
Answer is S = set(3, S1, set(8, S3, S4))
©D. Poole 2021
CPSC 312 — Lecture 33 9 / 19
Clicker Question
What is the resolution of the generalized answer clause: yes(B, N) :- append(B, [a, N|R], [b, a, c, d]).
with the clause append ([], L, L).
A yes([], c) :- append(B, R, [d])
B yes([b],c):-
C yes([b|T1],N) :- append(T1,[a,N|R],[a,c,d]).
D yes([b],N):-append([],[a,N|R],[a,c,d]).
E the resolution fails (they do not resolve)
©D. Poole 2021
CPSC 312 — Lecture 33 10 / 19
Clicker Question
What is the resolution of the generalized answer clause: yes(B, N) :- append(B, [a, N|R], [b, a, c, d]).
with the clause
append([H1 | T1],A1,[H1 | R1]) :-
append(T1,A1,R1).
A yes([], c) :- append(B, R, [d])
B yes([b],c):-
C yes([b|T1],N) :- append(T1,[a,N|R],[a,c,d]).
D yes([b],N):-append([],[a,N|R],[a,c,d]).
E the resolution fails (they do not resolve)
©D. Poole 2021
CPSC 312 — Lecture 33 11 / 19
Clicker Question
What is the resolution of the generalized answer clause: yes([b|T1],N) :- append(T1,[a,N|R],[a,c,d]).
with the clause append ([], L, L).
A yes([], c) :- append(B, R, [d])
B yes([b],c):-
C yes([b|T1],N) :- append([],[a,c,d],[a,c,d]).
D yes([b],N):-append([],[a,N|R],[a,c,d]).
E the resolution fails (they do not resolve)
©D. Poole 2021
CPSC 312 — Lecture 33 12 / 19
Unification with function symbols
Consider a knowledge base consisting of one fact: lt(X , s(X )).
Should the following query succeed? ?- lt(Y,Y).
What does the top-down proof procedure give?
Solution: variable X should not unify with a term that contains X inside. “Occurs check”
E.g., X should not unify with s(X).
Simple modification of the unification algorithm, which Prolog does not do!
CPSC 312 — Lecture 33 13 / 19
©D. Poole 2021
Equality
Equality is a special predicate symbol with a standard domain-independent intended interpretation.
Suppose interpretation I = ⟨D, φ, π⟩.
t1 and t2 are ground terms then t1 = t2 is true in interpretation I if t1 and t2 denote the same individual. That is, t1 = t2 if φ(t1) is the same as φ(t2).
t1 ̸= t2 when t1 and t2 denote different individuals.
Example:
D = {,,}.
φ(phone) = , φ(pencil) = , φ(telephone) = What equalities and inequalities hold?
phone = telephone, phone = phone, pencil = pencil, telephone = telephone
pencil ̸= phone, pencil ̸= telephone
Equality does not mean similarity!
CPSC 312 — Lecture 33
14 / 19
©D. Poole 2021
Equality
Constants/Terms
Individuals
a b c
d
f(a)
e
©D. Poole 2021
CPSC 312 — Lecture 33 15 / 19
Inequality as a subgoal
What should the following query return? ?− X̸=4.
What should the following query return? ?− X̸=4,X=7.
What should the following query return? ?− X̸=4,X=4.
Prolog has 3 different inequalities that differ on examples like these:
\== \= dif()
They differ in cases where there are free variables, and terms unify but are not identical.
CPSC 312 — Lecture 33 16 / 19
©D. Poole 2021
3 implementations of not-equals
Prolog has 3 different inequalities:
\== \= dif()
which give same answers for variable-free queries, or when both sides are identical
a \== 3, a \= 3, dif(a,3)
all succceed.
a \== a, a \= a, dif(a,a)
all fail.
They give different answers when there is a free variable. \== means “not identical”. a \== X succeeds
\= means “not unifiable”. a \= X fails
dif is less procedural and more logical
CPSC 312 — Lecture 33 17 / 19
©D. Poole 2021
Implementing dif
dif(X,Y)
all instances fail when X and Y are identical
all instances succeed when X and Y do not unify otherwise some instance succeed and some fail
To implement dif (X , Y ) in the body of a clause:
Select leftmost clause — unless it is a dif which cannot be
determined to fail or succeed (delay dif calls)
Return the dif calls not resolved.
Consider the calls:
dif(X,4), X=7.
dif(X,4), X=4.
dif(X,4), dif(X,7).
CPSC 312 — Lecture 33
18 / 19
©D. Poole 2021
Functional and logic programming
Unifying ideas:
specify what not how
program by thinking about the problem, not about the computation
variables don’t change their values once assigned — referential transparency
Haskell:
strong typing
higher-order functions allow us to create our own abstractions
lazy computation Prolog:
unification allows for powerful pattern matching non-determinism through search
extends relational databases
Programming at a high-level can help no matter what language you use!
CPSC 312 — Lecture 33 19 / 19
©D. Poole 2021