CS计算机代考程序代写 AI interpreter Reasoning with Variables

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 — Pre Lecture 32 1/9
©D. Poole 2021

Unifiers
Substitution σ is a unifier of e1 and e2 if e1σ = e2σ.
CPSC 312 — Pre Lecture 32 2/9
©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 — Pre Lecture 32 2/9
©D. Poole 2021

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 — Pre Lecture 32 3/9

Top-down Propositional Proof Procedure (recall)
Idea: search backward from a query to determine if it is a logical consequence of KB.
CPSC 312 — Pre Lecture 32 4/9
©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 — Pre Lecture 32 4/9
©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.
CPSC 312 — Pre Lecture 32 5/9
©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 — Pre Lecture 32 5/9
©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 — Pre Lecture 32 6/9

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
©D. Poole 2021
CPSC 312 — Pre Lecture 32 7/9

Example
parent(X,Y) :- mother(X,Y).
parent(X,Y) :- father(X,Y).
grandmother(X,Z) :-
mother(X,Y), parent(Y,Z).
father(pierre, justin).
mother(margaret, justin).
mother(estelle,sophie).
mother(sophie, xavier).
mother(sophie, ella_grace).
?- grandmother(estelle,X).
©D. Poole 2021
CPSC 312 — Pre Lecture 32 8/9

Related Posts