Exercise � We consider (undirected) graphs as structures of the form G = ⟨V, E⟩ where E is the
binary edge relation. Express the following statements in first-order logic.
(a) All vertices are neighbours.
(b) The graph contains a triangle.
(c) Every vertex has exactly three neighbours.
(d) Every pair of vertices is connected by a path of length at most .
Exercise � 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 � 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
(1) transform it into Skolem normal form;
(2) transform it into a set of clauses.
Exercise � 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) ∀xR(x, f (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)))
1
Exercise � 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, x, x) ,
∀x∀y∀z∀w[R(x, f (y, z), w) → R(f (y, x), z, w)] ,
¬∀x∀y[R(f (x, f (y, c)), c, f (y, f (x, c)))] .
2