Exercise 1 Let f be a binary function symbol, g, h unary, and c a constant symbol.
(a) Find the most general unifier for the following pairs of terms.
(i) f (g(x), y) and f (x, h(y))
(ii) f (h(x), x) and f (x, h(y))
(iii) f (x, f (x, g(y))) and f (y, f (h(c), x))
(iv) f (f (x, c), g(f (y, x))) and f (x, g(x))
(b) Solve the following set of term equations
x = f (y, z) , y = g(u) , z = h(y) , u = f (v, w) , v = f (c, w) .
Exercise 2 Consider the following formulae.
(a) ∃x∃y∀z[z = x ∨ z = y]
(b) ∀x[∃yR(x, y) → ∃yR(y, x)]
(c) ∀x[∀y∃z[R(x, f (y, z))] → ∀y∀z[R(f (x, y), f (x, z)) ∨ R(y, z)]]
(d) ∃x∀yR(x, y) ∧ ∀x∃yR(x, y) ∧ ∀x∀y[R(x, y) → ∃z[R(x, z) ∧ R(z, x)]]
For each of them
() transform it into Skolem normal form;
() transform it into a set of clauses.
Exercise 3 Use the resolution method to check that the following formulae are inconsistent.
(a) ∀x∀y[x ≤ y → (P(x) ↔ P(y))] ∧ ∀x∀y[x ≤ y ∨ y ≤ x] ∧ ∃xP(x) ∧ ∃x¬P(x)
(b) ∀x∃y[y ≤ x ∧ ¬E(x, y)] ∧ ∀x∀y[x ≤ y ∧ y ≤ x → E(x, y)] ∧ ∃x∀y[x ≤ y]
(c) ∀x∀y[R(x, y) → (P(x) ↔ ¬P(y))]∧∀x∀y[R(x, y) → ∃z[R(x, z)∧R(z, y)]]∧∃x∃yR(x, y)
(d) ∀x[R(x, f (x))∧E(x, x)]∧∀x∀y∀z[R(x, y)∧R(y, z) → R(x, z)]∧∀x∀y[E(x, y) → ¬R(x, y)]
∧ ∃xE(x, f (f (x)))

Exercise 4 Use SLD resolution to check that the following set of Horn-formulae is inconsistent.
(a) ∀xT(x, x) ,
∀x∀y∀z[E(x, y) ∧ T(y, z) → T(x, z)] ,
E(a, b) ,
E(b, c) ,
E(c, d) ,
¬T(a, d) .
(b) ∀xT(x, x) ,
∀x∀y∀z[T(x, y) ∧ E(y, z) → T(x, z)] ,
E(a, b) ,
E(b, c) ,
E(c, d) ,
¬T(a, d) .
(c) R(c, c) ,
∀x∀y∀z[R(x, f (y, z)) → R(f (y, x), z)] ,
¬∀x∀y[R(f (x, f (y, c)), f (y, f (x, c))] .
