Notes - Logic and Proof MT24, Unification and resolution

A substitution is a map

on the set of $\sigma$-terms such that

• $c\theta = c$ for each constant $c$ (function application is written on the right)
• $f(t _ 1, \ldots, t _ k) \theta = f(t _ 1 \theta, \ldots, t _ k \theta)$ for each $k$-ary function symbol

Therefore a substitution is determined by its action on variables.

An ordered pair of terms $s \stackrel?= t$.

• $\theta$ is a unifier if for all $1 \le i \le n$, $s _ i \theta = t _ i \theta$.
• $\theta$ is a most general unifier if for all unifiers $\theta’$, $\theta’$ “factors through” $\theta$, i.e. $\theta’ = \theta \theta’’$ for some substitution $\theta’$.

• Unifier: $\theta’ = [f(a)/x][a/y]$
• Most general unifier: $\theta = [f(y)/x]$.

@example~

It is in the form

where each $x _ i$ are distinct variables that do not appear in any term $t$. Such a system is said to be solved because deriving a most general unifier is easy:

Consider the set of equations

Then it’s clear that an mgu is

@example~

Let $S$ be the system of term equation. Non-deterministically apply the following rewrite rules to either convert $S$ into a solved system or into $\bot$, representing a system that it’s impossible to solve.

• Simplify: $\{x \stackrel?= x\} \cup S \implies S$ for any variable $S$
• Swap: $\{t \stackrel?= x\} \cup S \implies \{x \stackrel?= t\} \cup S$ if $t$ is not a variable
• Decompose: $\{f(s _ 1, \ldots, s _ n) \stackrel?= f(t _ 1, \ldots, t _ n)\} \cup S \implies \{s _ 1 \stackrel?= t _ 1, \ldots, s _ n \stackrel?= t _ n\} \cup S$
• Conflict: $\{f(s _ 1, \ldots, s _ m) \stackrel?= g(t _ 1, \ldots, t _ n)\} \cup S \implies \bot$ if $f \ne g$ ($f$ and $g$ can also be constants, i.e. $0$-ary functions)
• Elim: $\{x \stackrel?= t\} \cup S \implies \{x \stackrel?= t\} \cup S[t/x]$ if $x$ occurs in $S$ and not in $t$
• Occur: $\{x \stackrel?= t\} \cup S \implies \bot$ if $x$ is a proper subterm of $t$

(Mnemonic: Martelli and Montanari were SSD CEOs)

We prove that given a system $S$ of term equations, there is no infinite sequence of rewrites $S = S _ 1 \implies S _ 2 \implies S _ 3 \implies \cdots$, so that a maximal chain of rewrites starting from $S$ either ends in $\bot$ in a solved system $T$.

Note that $\mathbb N^3$ is well-ordered under the lexicographic order (i.e. there are no infinite decreasing terms). For each system $S$, associate a rank $(n _ 1, n _ 2, n _ 3) \in \mathbb N^3$ where:

• $n _ 1$ is the number of variables in $S$ that are not solved (where a variable is solved if it appears once in $S$ with the single occurrence being in an equation of the form $x \stackrel?= t$)
• $n _ 2$ is the total size of all terms occurring in $S$
• $n _ 3$ is the number of equations in $S$ of the form $t \stackrel?= x$ with $t$ not a variable

Then, each rule that doesn’t lead immediately to termination decreases the rank of the system:

• Simplify does not increase $n _ 1$ and decreases $n _ 2$
• Swap increases neither $n _ 1$ or $n _ 2$ and decreases $n _ 3$
• Decompose does not increase $n _ 1$ and decreases $n _ 2$
• Elim decreases $n _ 1$

Hence the algorithm must terminate.

On termination we either have $\bot$ or a solved system. Since each rule preserves the set of unifiers of the system, it follows that any unifiable set of literals $D$ has a most general unifier.

For termination, note that in any iteration of the while loop that does not cause termination, a variable $x$ is replaced everywhere in $D\theta$ by a term $t$ that does not contain $x$.

Thus the number of different variables occurring in $D\theta$ decreases by one in each iteration, and so the loop must terminate.

For correctness, consider the loop invariant that:

For any unifier $\theta’$ of $D$, we have $\theta’ = \theta \theta’$.

The invariant is established by the initial assignment of the identity substitution to $\theta$.

Now suppose that the invariant holds before at the start of an iteration. Suppose we find an occurrence of variable $x$ in a literal in $D\theta$ such that a different term $t$ occurs in the same position in another literal in $D\theta$.

From the invariant, we know that $\theta’$ is a unifier of $D\theta$, and thus $t\theta’ = x\theta’$. It follows that $\theta’ = [t/x]\theta’$. Thus the loop invariant is maintained by the assignment $\theta = \theta[t/x]$.

The negation of the while loop condition along with the invariant implies that the final value of $\theta$ is a most general unifier of $D$. The invariant also implies that if $\theta’$ is a unifier of $D$, then it is also a unifier of $D\theta$.

Because the algorithm only outputs “fail” if $D\theta$ has no unifier, it follows $D$ has no unifier.

Robinson’s unification algorithm for finding a most general unifier of a set of literals $D$ is as follows:

Input: a set of literals D
Output: a most general unifier of D or "fail"

theta = identity substitution
while D is not a singleton:
	pick two distinct literals in D and find the left-most positions at which they differ
	if one of the corresponding sub-terms is a variable x and the other a term t not containing x:
		D = D[t/x],
		theta = theta[t/x]
	else:
		output "fail", halt

The first discrepancy is

and so we need to apply the substitution $[f(z) / x)]$. This gives the set

and so we need to apply the substitution $[f(z)/y]$ to $D’$ to yield the singleton

Thus

is a most general unifier of $D$.

@example~

Two cases.

Case 1, $C _ 1$ and $C _ 2$ have no variables in common: $R$ is a resolvent of $C _ 1$ and $C _ 2$ if there are sets of literals $D _ 1 \subseteq C _ 1$ and $D _ 2 \subseteq C _ 2$ such that

has a most general unifier $\theta$ and

where $L = D _ 1 \theta$ and $\overline L = D _ 2 \theta$.

Case 2, $C _ 1$ and $C _ 2$ do have variables in common: $R$ is a resolvent of $C _ 1$ and $C _ 2$ if there are variable renaming $\theta _ 1$ and $\theta _ 2$ such that $C _ 1 \theta _ 1$ and $C _ 2 \theta _ 2$ have no variable in common and $R$ is a resolvent of $C _ 1 \theta _ 1$ and $C _ 2 \theta _ 2$ according to the above.

First, apply the substitution $[u/x]$ to $C _ 1$ to obtain a clause $C _ 1’$ that has no variable in common with $C _ 2$. Now unify complementary literals under the substitution $[e/x][u/y][g(e)/z]$, obtaining $\{\lnot P(e, u, g(e))\}$.

@example~

A sequence of clauses $C _ 1, \ldots, C _ m$ with $C _ m = C$ such that each $C _ i$ is either a clause of $F$ (possibly with the variables renamed) or it follows by a resolution step from two preceding clauses.

This is equivalent to showing that $F _ 1 \land F _ 2 \land \lnot F _ 3$ is unsatisfiable. By the completeness of predicate logic resolution, there must be a derivation of $\square$ from the corresponding clauses $\{F _ 1, F _ 2, \lnot F _ 3\}$.

Skolemise each formula:

• $F _ 1$ is already in Skolem form
• $F _ 2$ is already in Skolem form
• Skolemising $\lnot F _ 3$ leads to the equisatisfiable formula $G _ 3 = \forall z \lnot A(s(s(e)), c, z)$ where $c$ is a new constant symbol.

Then $F _ 1 \land F _ 2 \land G _ 3$ is equisatisfiable with $F _ 1 \land F _ 2 \land \lnot F _ 3$, so it suffices to give a resolution refutation of $F _ 1 \land F _ 2 \land G _ 3$.

Derive the empty clause using resolution:

Since resolution requires distinct variables, we lay out the proof on several lines where each variable is subscripted by the line number (this is equivalent to applying the corresponding substitution).

1. Clause of $G _ 3$: $\{ \lnot A(s(s(e)), c, z _ 1) \}$
2. Clause of $F _ 2$: $\{\lnot A(x _ 2, y _ 2, z _ 2), A(s(x _ 2), y _ 2, s(z _ 2))\}$
3. 1,2 Res with $\theta = [s(e)/x _ 2][c/y _ 2][s(z _ 2)/z _ 1][z _ 3/z _ 2]$: $\{ \lnot A(s(e), c, z _ 3) \}$
4. 2,3 Res with $\theta = [e/x _ 2][c/y _ 2][s(z _ 2)/z _ 3][z _ 4/z _ 3]$: $\{\lnot A(e, c, z _ 4)\}$
5. Clause of $F _ 1$: $\{A(e, y _ 5, y _ 5)\}$
6. 4,5 Res with $[c/y _ 5][c/z _ 4]$: $\square$

as required.

@example~

Suppose:

• $F = \forall x _ 1 \cdots \forall x _ n G$ is a closed formula in Skolem form where $G$ is quantifier free
• $R$ is a resolvent of two clauses in $G$

Then:

• $F \equiv \forall^\ast (G \cup \{R\})$ (where $\forall^\ast$ denotes the universal closure)

Note that $\forall^\ast (G \cup \{R\}) \models F$ since $\forall^\ast G \models F$.

For the other direction, we need to show that $F \models \forall^\ast R$. Since $F$ is closed, it suffices to show that $F \models R$ (@todo).

Suppose that $R$ is a resolvent of clauses $C _ 1, C _ 2 \in G$ with

for some substitutions $\theta$ and $\theta’$ and complementary literals $L \in C _ 1 \theta$ and $\overline L \in C _ 2 \theta’$.

Let $\mathcal A$ be an assignment that satisfies $F = \forall^\ast G$. Since $C _ 1, C _ 2 \in G$, by the translation lemma, $\mathcal A \models C _ 1 \theta$ and $\mathcal A \models C _ 2 \theta’$.

Since $\mathcal A’$ satisfies at most one of the complementary literals $L$ and $\overline L$, it follows that $\mathcal A$ satisfies at least one of $C _ 1 \theta \setminus \{L\}$ and $C _ 2 \theta’ \setminus \{L’\}$.

Therefore $\mathcal A$ satisfies $R$, as required.

Suppose:

• $F = \forall x _ 1 \cdots \forall x _ n G$ is a closed formula in Skolem form
• $C$ is a clause obtained from $G$ by a resolution derivation

Then

Suppose:

• $F$ is a closed formula in Skolem form with its matrix $G$ in CNF
• $G$ is unsatisfiable

Then:

• There is a predicate-logic resolution proof of $\square$ from $G$.