Home assignment 1 : Margus Martsepp 121843IAPM Propositional logic and simple predicate assignments Advanced Course of Applied Logics ( ITV0081 ) Task 1: Code Task 1: Results Task 2: Code Task 2: Result Task 3: Code Task 3: Result Task 3: Proof - distribution of intersection over union. Task 3: Extra proof - distribution of union over intersection. Task 4: Code Task 4: Result Task 5: Code
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)) s(big,rat) | ~s(small,hamster) Task 3 List all the resolvants of the following two clauses: p...
annaabi.ee 
