Version without JavaScript, read-only: workshops, quizzes and running code are not available here. Full version · Catalogue · Sign in
Lecture notes · chapter 10
Unification and first-order resolution
Finding the most general substitution that makes two terms equal, using it to resolve clauses with variables, and what the machine can, or cannot, decide.
The problem
The clauses $\lnot \mathit{Homme}(x) \lor \mathit{Mortel}(x)$ and $\mathit{Homme}(\mathit{socrate})$ should give $\mathit{Mortel}(\mathit{socrate})$. But the rule of chapter 5 requires a literal and its exact opposite, and $\mathit{Homme}(x)$ is not $\mathit{Homme}(\mathit{socrate})$. Since the variable $x$ of the first clause stands for every object (it is implicitly quantified by $\forall$), we can specialise it: by replacing $x$ with $\mathit{socrate}$, the two literals become opposite. Finding this replacement is called unification.
Substitutions and unifiers
Substitution
A substitution $\sigma = \{x_1 := t_1, \ldots, x_n := t_n\}$ replaces simultaneously each variable $x_i$ by the term $t_i$. We write $t\sigma$ for the result on a term $t$ (and $L\sigma$ on a literal).
Example: $f(x, g(y))\{x := a,\; y := h(x)\} = f(a, g(h(x)))$. The $x$ brought in by $h(x)$ is not replaced in turn: the replacement is simultaneous.
Unifier
A unifier of two terms (or of two atoms) $s$ and $t$ is a substitution $\sigma$ such that $s\sigma = t\sigma$.
$f(x, a)$ and $f(b, y)$ have the unifier $\{x := b, y := a\}$: both become $f(b, a)$.
Two terms can have many unifiers. $g(x)$ and $g(y)$ are unified by $\{x := y\}$, but also by $\{x := a, y := a\}$, which says more than necessary. We look for the most general unifier (mgu for short): the one that fixes only what is indispensable, and of which all the others are special cases. Here, $\{x := y\}$.
The unification algorithm
We start from the equation $s = t$ and apply these rules as long as we can, to a set of equations (Robinson's algorithm, 1965, in the form given by Martelli and Montanari):
| Rule | If we have | We do |
|---|---|---|
| Decompose | $f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)$ | replace it by $s_1 = t_1, \ldots, s_n = t_n$ |
| Clash | $f(\ldots) = g(\ldots)$, with $f \neq g$ (or different constants) | failure |
| Delete | $t = t$ | remove the equation |
| Orient | $t = x$, where $t$ is not a variable | turn it round: $x = t$ |
| Occurs check | $x = t$, where $x$ occurs in $t$ (and $t \neq x$) | failure |
| Eliminate | $x = t$, where $x$ does not occur in $t$ | replace $x$ by $t$ in all the other equations |
At the end, if there has been no failure, equations $x_1 = t_1, \ldots, x_n = t_n$ remain: that is the mgu.
First-order resolution
The rule
Take two clauses with no variable in common (renaming if needed), $C \lor P(s_1, \ldots, s_n)$ and $D \lor \lnot P(t_1, \ldots, t_n)$. If $P(s_1, \ldots, s_n)$ and $P(t_1, \ldots, t_n)$ have an mgu $\sigma$, the resolvent is:
The substitution is applied to everything that remains, not only to the resolved literals.
Full resolution also uses factoring: if two literals of the same clause are unifiable, they can be merged, by applying their mgu to the clause. It is rarely needed in the exercises.
Theorem (Robinson, 1965). A set of first-order clauses is unsatisfiable if and only if $\square$ can be derived from it by resolution and factoring. (Admitted.)
The complete method
To show $\Sigma \vDash A$:
- take $\Sigma \cup \{\lnot A\}$;
- put each formula in prenex form, Skolemise, turn into clauses (chapter 9);
- rename the variables so that no clause shares any with another;
- derive $\square$ by resolution, unifying at each step.
What the machine can decide
In propositional calculus, validity is decidable: a truth table always answers, even if slowly. In first order, this is no longer the case.
Theorem (Church and Turing, 1936). There is no algorithm which, for every first-order formula, decides whether it is valid.
Resolution nevertheless gives a semi-decision: if the formula is valid, the search will eventually find $\square$; if it is not, the search may never stop. That is the best one can do.
Prolog exploits this situation. A Prolog program is a set of first-order Horn clauses, a query is a goal to refute, and the interpreter performs resolution with unification, in a fixed order. By default, it omits the occurs check, to go faster: it then agrees to unify X and f(X), which the algorithm of this chapter refuses.
What we have done
The course followed a single thread: knowing whether a statement follows from others. We set it up on propositions, by reading formulas (chapter 1) and giving them a meaning (chapter 2). We learnt to transform them (chapter 3), to have them solved (chapter 4), to refute them (chapter 5) and to prove them (chapter 6). Then we took everything up again with objects and quantifiers (chapters 7 to 10), up to the limit of what a machine can decide.