Version without JavaScript, read-only: workshops, quizzes and running code are not available here. Full version · Catalogue · Sign in

Exercise sheet 10

First-order unification and resolution

Compute most general unifiers, refute with variables, and follow what Prolog does. Chapter 10.

Solution
  1. $\{x := b,\; y := a\}$.
  2. Decompose: $x = f(y)$, $f(x) = z$. Eliminate $x$: $z = f(f(y))$. mgu: $\{x := f(y),\; z := f(f(y))\}$.
  3. Failure by the occurs check: we reach $y = f(f(y))$ (see chapter 10).
  4. Failure by clash: $a = b$, two different constants.
  5. $\{x := g(g(a)),\; y := g(a),\; z := a\}$.
  6. $x = f(y)$ and $x = f(a)$. Eliminate $x$: $f(y) = f(a)$, then $y = a$. mgu: $\{x := f(a),\; y := a\}$.
Solution
  1. Clauses $\lnot \mathit{Homme}(x) \lor \mathit{Mortel}(x)$, $\mathit{Homme}(s)$, $\lnot \mathit{Mortel}(s)$. Resolving the first two with $\{x := s\}$: $\mathit{Mortel}(s)$; with the third: $\square$.
  2. Clauses: (1) $\lnot C(x) \lor G(x)$, (2) $\lnot C(y) \lor \mathit{Car}(y)$, (3) $C(a)$, (4) $\lnot \mathit{Car}(z) \lor \lnot G(z)$. (1) and (3), $\{x := a\}$: (5) $G(a)$. (2) and (3), $\{y := a\}$: (6) $\mathit{Car}(a)$. (4) and (6), $\{z := a\}$: (7) $\lnot G(a)$. (5) and (7): $\square$.
  3. Predicates $E$, $T$, $R$, $H$ (student, works, passes, happy), constant $m$. Clauses: (1) $\lnot E(x) \lor \lnot T(x) \lor R(x)$, (2) $\lnot E(y) \lor \lnot R(y) \lor H(y)$, (3) $E(m)$, (4) $T(m)$, (5) $\lnot H(m)$. (2) and (5), $\{y := m\}$: (6) $\lnot E(m) \lor \lnot R(m)$; with (3): (7) $\lnot R(m)$. (1) and (7), $\{x := m\}$: (8) $\lnot E(m) \lor \lnot T(m)$; with (3): (9) $\lnot T(m)$; with (4): $\square$.
Solution
  1. $\mathit{parent}(\mathit{tom}, \mathit{bob})$; $\mathit{parent}(\mathit{bob}, \mathit{ann})$; $\lnot \mathit{parent}(X, Y) \lor \lnot \mathit{parent}(Y, Z) \lor \mathit{grandparent}(X, Z)$.
  2. Goal $\lnot \mathit{grandparent}(\mathit{tom}, W)$ with the third clause, mgu $\{X := \mathit{tom},\; Z := W\}$: $\lnot \mathit{parent}(\mathit{tom}, Y) \lor \lnot \mathit{parent}(Y, W)$. With $\mathit{parent}(\mathit{tom}, \mathit{bob})$, $\{Y := \mathit{bob}\}$: $\lnot \mathit{parent}(\mathit{bob}, W)$. With $\mathit{parent}(\mathit{bob}, \mathit{ann})$, $\{W := \mathit{ann}\}$: $\square$. Prolog answers W = ann: the value that unification gave to $W$ along the way.
Solution
  1. We would set $x := f(x)$, and the resulting term would be infinite: $f(f(f(\ldots)))$. No finite term fits: unification must fail.
  2. They are not contradictory: over $\mathbb{N}$ with $P$ as equality and $f$ as “plus one”, $\forall x\, P(x, x)$ is true, and so is $\forall y\, \lnot P(y, f(y))$ ($y \neq y + 1$). Yet, without the occurs check, we would unify $P(x, x)$ and $P(y, f(y))$ by setting $x := y$ then $y := f(y)$, and we would derive $\square$: a “proof” of a contradiction that does not exist. That is the price of Prolog's speed.