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 Today
Unification and Proofs.
CPSC 312 — Lecture 32 1 / 13
©D. Poole 2021
Reasoning with Variables
An instance of an atom or a clause is obtained by uniformly substituting terms for variables. Every instance of the same variable is replaced by the same term.
A substitution is a finite set of the form {V1/t1, . . . , Vn/tn}, where each Vi is a distinct variable and each ti is a term.
The application of a substitution σ = {V1/t1, . . . , Vn/tn} to an atom or clause e, written eσ, is the instance of e with every occurrence of Vi replaced by ti .
CPSC 312 — Lecture 32 2 / 13
©D. Poole 2021
Application Examples
The following are substitutions:
σ1 = {X/A,Y/b,Z/C,D/e}
σ2 = {A/X,Y/b,C/Z,D/e}
σ3 = {A/V,X/V,Y/b,C/W,Z/W,D/e}
The following shows some applications: p(A,b,C,D)σ1 = p(A,b,C,e) p(X,Y,Z,e)σ1 = p(A,b,C,e) p(A,b,C,D)σ2 = p(X,b,Z,e) p(X,Y,Z,e)σ2 = p(X,b,Z,e) p(A,b,C,D)σ3 = p(V,b,W,e) p(X,Y,Z,e)σ3 = p(V,b,W,e)
©D. Poole 2021
CPSC 312 — Lecture 32 3 / 13
Application Examples
Given the substitution:
σ = {X/A,Y/b,Z/C,D/e}
foo(D,Z,C,A)σ is A foo(D,Z,C,A) B foo(e,C,C,A) C foo(D,C,C,X) D foo(e,C,C,X) E foo(e,C,Z,A)
©D. Poole 2021
CPSC 312 — Lecture 32 4 / 13
Application Examples
Given the substitution:
σ = {X/A,Y/b,Z/C,D/e}
foo(W,b,C,A)σ is A foo(X,Y,Z,D) B foo(b,b,C,Y) C foo(W,Y,C,X) D foo(W,b,C,A) E foo(W,Y,C,A)
©D. Poole 2021
CPSC 312 — Lecture 32 5 / 13
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 32 6 / 13
©D. Poole 2021
Unification Example
A yes
B no
C I’m not sure Is the substitution a unifier of p(A,b,C,D) and p(X,Y,Z,e):
σ1 = {X/A,Y/b,Z/C,D/e}
σ2 ={Y/b,D/e}
σ3 = {X/A,Y/b,Z/C,D/e,W/a}
σ4 = {A/X,Y/b,C/Z,D/e}
σ5 = {X/a,Y/b,Z/c,D/e}
σ6 = {A/a,X/a,Y/b,C/c,Z/c,D/e}
σ7 = {A/V,X/V,Y/b,C/W,Z/W,D/e} σ8 = {X/A,Y/b,Z/A,C/A,D/e}
Which are most general unifiers?
yes no yes yes no yes yes yes σ1, σ4
©D. Poole 2021
CPSC 312 — Lecture 32 7 / 13
1: 2: 3: 4: 5: 6: 7: 8: 9:
10: 11: 12: 13: 14: 15: 16:
17:
procedure unify(t1,t2) E := {t1 = t2}
S := {}
while E ̸= {} do
◃ Returns mgu of t1 and t2 or ⊥. ◃ Set of equality statements ◃ Substitution
select and remove x = y from E if y is not identical to x then
if x is a variable then
replace x with y in E and S S := {x/y} ∪ S
else if y is a variable then replace y with x in E and S S := {y/x} ∪ S
else if x is p(x1,…,xn) and y is p(y1,…,yn) then E := E ∪ {x1 = y1, . . . , xn = yn}
else
return ⊥ ◃ t1 and t2 do not unify
returnS
◃S ismguoft1 andt2
©D. Poole 2021
CPSC 312 — Lecture 32 8 / 13
Examples
unify p(A,b,C,D) and p(X,Y,Z,e) {A/X,Y/b,C/Z,D/e}
unify p(A,b,A,D) and p(X,X,Z,Z) {A/b,X/b,Z/b,D/b}
unify p(A,b,A,d) and p(X,X,Z,Z) ⊥
unify n([sam,likes,prolog],L2,I,C1,C2) and n([P|R],R,P,[person(P)|C],C)
{P/sam, R/[likes,prolog], L2/[likes,prolog], I/sam, C1/[person(sam)|C2], C/C2}
CPSC 312 — Lecture 32
9 / 13
©D. Poole 2021
Top-down Propositional Proof Procedure (recall)
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 32 10 / 13
©D. Poole 2021
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 32 11 / 13
©D. Poole 2021
Top-down propositional definite clause interpreter (recall)
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 32 12 / 13
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 a1 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 32 13 / 13