Experimenting with predicate provers. (0)

 
 
 
 
 
 
 
 
Home assignment 3 : Margus Martsepp 121843IAPM 
Experimenting with 
predicate provers. 
Advanced Course  of Applied Logics ( ITV0081 ) 
 
 
Part  A : Warmers 
Task 1 
What is the most general unifier of the  following  atoms: 
p(X,f(Y),Z) 
p(T,T,g(cat)) 
p(f(dog),S,g(W)) 
 
solution : 
Θ 
 
 
Task 2 
List all the  binary  resolvants of the following two  clauses : 
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T) 
~p(f(dog),S,g(W)) | s(big,rat) | ~s(small, hamster ) 
 
solution sourse: 
1st option  (1.4-2.2) 
Θ 
p(X,f(Y),big) | p(rat,rat,g(cat)) | r(X,rat) 
~p(f(dog),S,g(W)) | ~s(small,hamster) 
 
2nd option (1.1-2.1) 
Θ 
p(T,T,g(cat)) | r(f(dog),T) | ~s(g(W),T) 
s(big,rat) | ~s(small,hamster) 
 
 
3rd option (1.2-2.1) 
Θ 
p(X,f(Y),Z) | r(X,f(dog)) | ~s(Z,f(dog)) 
s(big,rat) | ~s(small,hamster) 
 
 
Task 3 
List all the resolvants of the following two clauses: 
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T) 
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster) 
 
 
solution sourse: 
1st option - See binary resolution 1st option 
2nd option - See binary resolution 2nd option 
3rd option - See binary resolution 3rd option 
 
4th option ((1.1+1.2)-2.1) 
Θ 
p(f(Y),f(Y),g(cat)) | r(f(Y),f(Y)) | ~s(g(cat),f(Y)) 
~p(f(dog),S,g(W)) | s(big,rat) | ~s(small,hamster) 
 
 
Θ 
r(f(dog),f(dog)) | ~s(g(cat),f(dog)) 
s(big,rat) | ~s(small,hamster) 
 
 
5th option (1.4+2.3) 
Θ 
p(X,f(Y),small) | p(hamster,hamster,g(cat)) | r(X,hamster)  
~p(f(dog),S,g(W)) | s(big,rat) | ~s(small,hamster) 
 
 
Task 4 
List all the factors of the following  clause : 
p(X,f(Y),Z) | ~s(Z,T) | p(T,T,g(cat)) | p(f(dog),S,g(W)) | ~s(small,hamster) 
 
 
1st option 
Θ 
p(X,f(Y),small) | p(hamster,hamster,g(cat)) | p(f(dog),S,g(W)) | 
~s(small,hamster) 
 
 
2nd option 
Θ 
~s(g(cat),f(Y)) | p(f(Y),f(Y),g(cat)) | p(f(dog),S,g(W)) | ~s(small,hamster) 
 
 
3rd option 
Θ 
~s(g(W),T) | p(T,T,g(cat)) | p(f(dog),f(Y),g(W)) | ~s(small,hamster) 
 
 
4th option 
Θ 
p(X,f(Y),Z) | ~s(Z,f(dog)) | p(f(dog),f(dog),g(cat)) | ~s(small,hamster) 
 
 
5th option 
Θ 
~s(g(cat),f(dog)) | p(f(dog),f(dog),g(cat)) | ~s(small,hamster) 
 
 
6th option 
Θ 
~s(g(cat),f(dog)) | p(f(dog),f(dog),g(cat)) | ~s(small,hamster) 
 
 
 
Task 5 
One resolvant of the clauses: 
p(X,f(Y),Z) | p(T,T,g(cat)) | r(X,T) | ~s(Z,T) 
~p(f(dog),S,g(W) | s(big,rat) | ~s(small,hamster) 
is 
r(f(dog),f(dog)) | ~s(g(cat),f(dog)) | s(big,rat) | ~s(small,hamster) 
Show how that may be  formed  by factoring and binary resolution. 
 
 
Θ 
p(f(Y),f(Y),g(cat)) | r(f(Y),f(Y)) | ~s(g(cat),f(Y)) 
~p(f(dog),S,g(W)) | s(big,rat) | ~s(small,hamster) 
 
 
Θ 
r(f(dog),f(dog)) | ~s(g(cat),f(dog)) 
s(big,rat) | ~s(small,hamster) 
 
 
Task 6 
Use resolution to derive the empty clause from the set 
< 
 
 
solution: 
p(f(X)) | p(X)  
~p(X) | p(f(X)) 
 
 
p(f(X)) | p(f(X)) // resolution 
p(f(X))  
 
// factoring 
 
 
~p(X) | ~p(f(X)) 
p(f(X)) 
empty clause  
// resolution applied 2 times  
Task 7 
Draw the  failure  tree for the following set of clauses: 
< 
 
 
solution: 
<, 
Top, VertexLabeling -> True] 
 
 
 
Task 8 
Show the execution of the ANL  loop  to derive the empty clause from: 
< 
Use any  selection   strategy  you want, and number the chosen clause at each iteration. 
 
 
1st ply 
~r(Y) | ~p(Y) + p(b) 
= ~r(Y) 
~r(Y) | ~p(Y) + r(a) 
= ~p(Y)  
~r(Y) | ~p(Y) + p(S) | ~p(b) | ~r(S) 
= ~r(Y) | ~p(b) | ~r(S) = ~r(Y) | ~p(b) = ~r(S) | ~p(b) 
~r(Y) | ~p(Y) + r(c)  
= ~p(Y) 
p(S) | ~p(b) | ~r(S) + p(b) 
= p(S) | ~r(S)  
p(S) | ~p(b) | ~r(S) + r(a) 
= p(S) | ~p(b)  
p(S) | ~p(b) | ~r(S) + r(c) 
= p(S) | ~p(b) 
 
 
2nd ply 
~p(Y) + p(S) | ~p(b) | ~r(S) 
 
= ~p(b) | ~r(S) 
~r(Y) | ~p(b) + p(b) 
 
= ~r(Y) 
~r(Y) | ~p(b) + r(a) 
 
= ~p(b)  
~r(Y) | ~p(b) + p(S) | ~p(b) | ~r(S) 
 
= ~r(Y) | ~p(b) | ~r(S) 
~r(Y) | ~p(b) + r(c) 
 
= ~p(b)  
p(S) | ~r(S) + ~r(Y) | ~p(Y) 
 
= ~r(S) | ~r(Y) = ~r(S) = ~r(Y) 
p(S) | ~r(S) + r(a) 
= p(S) 
p(S) | ~r(S) + p(S) | ~p(b) | ~r(S) 
 
= ~r(S) 
p(S) | ~p(b) + ~r(Y) | ~p(Y) 
 
= ~p(b) | ~r(Y)  
 
 
Task 9 
Inspect if terms have unifiers and  find  the most general unifiers: 
1.  p(f(y), w, g(z)) and p(u, u, v); 
2.  p(f(y), w, g(z)) and p(v, u, v); 
3.  p(a, x, f(g(y))) and p(z, h(z, w), f(w)) 
 
 
1st option  
Θ 
p(f(y), f(y), g(z)) 
p(f(y), f(y), g(z)) 
 
 
2nd option 
Θ 
p(f(y), u, g(z))  
p(f(y), u, f(y)) 
does not have unifier 
 
 
3nd option 
Θ 
p(z, h(z, g(y)), f(g(y)))  
p(z, h(z, g(y)), f(g(y)))