Experimenting with predicate provers.
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:
= { X/T, S/T, T/f[Y], Z/g(cat), W/cat, dog/Y }
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)
= { Z/big, T/rat }
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)
= { X/f(dog), S/f(Y), Z/g(W) }
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)
= { T/f(dog), S/f(dog), W/cat }
p(X,f(Y),Z) | r(X,f(dog)) | ~s(Z,f(dog))
annaabi.ee 
