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 3.
Exercise � Let f be a binary function symbol, g,h unary, and c a constant symbol. Find the most
general unifier for the following pairs of terms.
(a) f(g(x),y) and f(x,h(y))
(b) f(h(x),x) and f(x,h(y))
(c) f(x,f(x,g(y))) and f(y,f(h(c),x))
(d) f(f(x,c),g(f(y,x))) and f(x,g(x))
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
(�) transform it into Skolem normal form;
(�) 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)))
�
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)))] .
�