Lecture 6: Unification and Lifting

Laura Kovács and Andrei Voronkov

First-Order Logic: Exercises

Which of the following statements are true?

1. First-order logic is an extension of propositional logic.
2. First-order logic is NP-complete.
3. In first-order logic you can use quantifiers over sets.
4. First-order logic is decidable.
5. One can axiomatise naturals in first-order logic.
6. Having proofs is good.

Substitution

• A substitution $\theta$ is a mapping from variables to terms such that the set $\{x \mid \theta(x) \neq x\}$ is finite.
• This set is the domain of $\theta$.
• Notation: $\{\,x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\,\}$, where $x_1,\ldots,x_n$ are pairwise different variables, denotes the substitution $\theta$ with $$\theta(x) = \begin{cases} t_i & \text{if } x = x_i,\\ x & \text{if } x \notin \{x_1,\ldots,x_n\}. \end{cases}$$
• Applying a substitution $\theta$ to an expression $E$ means replacing each $x_i$ by $t_i$ simultaneously; we denote the result by $E\theta$.
• Substitutions are functions, so we can compose them. We write $\sigma\tau$ (rather than $\tau \circ \sigma$), and we always have $E(\sigma\tau) = (E\sigma)\tau$.

Example

Consider the expression $E = p(x,y,f(a))$ and the substitution $\theta = \{x \mapsto b,\; y \mapsto x\}$.
What is $E\theta$?

Substitution Composition

Suppose we have two substitutions

$$\begin{aligned} \theta_1 &= \{x_1 \mapsto s_1,\ldots,x_m \mapsto s_m\},\\ \theta_2 &= \{y_1 \mapsto t_1,\ldots,y_n \mapsto t_n\}. \end{aligned}$$

How can we compute their composition $\theta_1\theta_2$?

The substitution $\theta_1\theta_2$ is obtained from

$$\{x_1 \mapsto s_1\theta_2,\ldots,x_m \mapsto s_m\theta_2,\; y_1 \mapsto t_1,\ldots,y_n \mapsto t_n\}$$

by deleting

1. all $y_i \mapsto t_i$ such that $y_i \in \{x_1,\ldots,x_m\}$;
2. all $x_i \mapsto s_i\theta_2$ such that $x_i = s_i\theta_2$.

The remaining bindings constitute $\theta_1\theta_2$.

Example

Let

$$\theta_1 = \{x \mapsto f(y),\; y \mapsto z\}, \qquad \theta_2 = \{x \mapsto a,\; y \mapsto b,\; z \mapsto y\}.$$

What is $\theta_1\theta_2$?

Instances and Ground Instances

An instance of an expression $E$ (term, atom, literal, or clause) is obtained by applying a substitution to $E$.

• Some instances of the term $f(x,a,g(x))$ are $f(x,a,g(x))$, $f(y,a,g(y))$, $f(a,a,g(a))$, and $f(g(b),a,g(g(b)))$.
• The term $f(b,a,g(c))$ is not an instance of $f(x,a,g(x))$.
• A ground instance is an instance that contains no variables.

Herbrand's Theorem

For a set of clauses $S$, let $S^*$ denote the set of ground instances of clauses in $S$.

Theorem. Let $\Sigma$ be a signature with at least one constant symbol and let $S$ be a set of universal clauses over $\Sigma$. The following are equivalent:

1. $S$ is unsatisfiable.
2. $S^*$ is unsatisfiable.

By compactness of first-order logic, this is equivalent to:

3. There exists a finite unsatisfiable set of ground instances of clauses in $S$.

Thus the theorem reduces checking unsatisfiability of arbitrary clause sets to checking unsatisfiability of sets of ground clauses, even though $S^*$ can be infinite.

Lifting

Lifting is a technique for proving completeness theorems:

1. Prove completeness of the inference system for sets of ground clauses.
2. Lift the proof to the non-ground case.

Lifting Example

Consider the non-ground clauses $p(x,a) \lor q_1(x)$ and $\neg p(y,z) \lor q_2(y,z)$. When the signature contains function symbols, both clauses have infinitely many ground instances:

$$\{\,p(r,a) \lor q_1(r) \mid r \text{ is ground}\,\}, \qquad \{\,\neg p(s,t) \lor q_2(s,t) \mid s,t \text{ are ground}\,\}.$$

We can resolve ground instances iff $r=s$ and $t=a$, yielding inferences such as

$$\frac{p(s,a) \lor q_1(s) \qquad \neg p(s,a) \lor q_2(s,a)}{q_1(s) \lor q_2(s,a)}(\text{BR}),$$

but there are infinitely many such inferences.

Lifting Idea

Represent an infinite number of ground inferences of the form:

$$\frac{p(s,a) \lor q_1(s) \qquad \neg p(s,a) \lor q_2(s,a)}{q_1(s) \lor q_2(s,a)}(\text{BR}),$$

with a single non-ground inference:

$$\frac{p(x,a) \lor q_1(x) \qquad \neg p(y,z) \lor q_2(y,z)}{q_1(y) \lor q_2(y,a)}(\text{BR}).$$ Is this always possible?

Yes!

For the inference

$$\frac{p(x,a) \lor q_1(x) \qquad \neg p(y,z) \lor q_2(y,z)}{q_1(y) \lor q_2(y,a)}(\text{BR}),$$

the substitution $\{x \mapsto y,\; z \mapsto a\}$ solves the “equation” $p(x,a) = p(y,z)$, so the lifted inference represents all its ground instances.

Lifting Lemma for $\mathbb{BR}$ (Robinson 1965)

Idea. Represent infinitely many ground inferences by a single non-ground inference.

For binary resolution $\mathbb{BR}$ with selection:

• Work with non-ground clauses.
• Generalize the notion of “same” ground atoms to unifiability of non-ground atoms.
• Compute most general unifiers (mgu) only.

🎬 Animation: See a most general unifier applied during first-order resolution.

Lifting Lemma. Let $C$ and $D$ be clauses that share no variables. If a ground binary resolution inference

$$\frac{C\sigma_1 \qquad D\sigma_2}{C'}(\text{ground BR})$$

exists, then there is a substitution $\sigma$ such that a non-ground inference

$$\frac{C \qquad D}{C''}(\text{BR})$$

and $C' = C''\sigma$.

Similar lifting lemmas exist for each inference of $\mathbb{BR}$ and of the superposition system $\mathbb{S}\mathrm{up}$.

What Should We Lift?

• The ordering $\succ$.
• The selection function $\sigma$.
• The calculus $\mathbb{S}\mathrm{up}^{\mathrm{sat}}$.

Most importantly, lifting requires solving equations $s = t$ between terms and between atoms, which we do using most general unifiers.

Unifier

A unifier of expressions $s_1$ and $s_2$ is a substitution $\theta$ with $s_1\theta = s_2\theta$.
Equivalently, it is a solution of the “equation” $s_1 = s_2$. For systems of equations $s_1 = s'_1,\ldots,s_n = s'_n$, a substitution that satisfies all equations simultaneously is a simultaneous unifier.

Most General Unifiers

A solution $\theta$ to a set of equations $E$ is most general if, for every other solution $\sigma$, there exists a substitution $\tau$ with $\theta\tau = \sigma$. In a similar way, we can define a most general unifier.

Consider the terms $f(x_1,g(x_1),x_2)$ and $f(y_1,y_2,y_2)$. Two unifiers are

$$\theta_1 = \{y_1 \mapsto x_1,\; y_2 \mapsto g(x_1),\; x_2 \mapsto g(x_1)\}, \qquad \theta_2 = \{y_1 \mapsto a,\; y_2 \mapsto g(a),\; x_2 \mapsto g(a),\; x_1 \mapsto a\}.$$

Both substitutions make the terms equal, but only $\theta_1$ is an mgu; $\theta_2$ is obtained from it by instantiating $x_1$ with $a$.

Unification Algorithm

Let $E$ be a set of equations. An isolated equation in $E$ is any equation $x = t$ in $E$ such that $x$ has exactly one occurrence in $E$.

Input. A finite set of equations $E$ (here $s,t$ denote terms, $c,d$ constants, $f,g$ function symbols, and $x$ a variable).

Output. A solution to $E$ or failure.

1. While there exists a non-isolated equation $(s = t) \in E$:
   • Consider the pair $(s,t)$.
     • $(t,t)$ $\Rightarrow$ remove this equation from $E$.
     • $(x,t)$ $\Rightarrow$
       • if $x$ occurs in $t$, halt with failure;
       • otherwise, replace every other occurrence of $x$ in $E$ by $t$.
     • $(t,x)$ $\Rightarrow$ replace this equation by $x = t$ and proceed as in $(x,t)$.
     • $(c,d)$ $\Rightarrow$ halt with failure.
     • $(c,f(t_1,\ldots,t_n))$ $\Rightarrow$ halt with failure.
     • $(f(t_1,\ldots,t_n),c)$ $\Rightarrow$ halt with failure.
     • $(f(s_1,\ldots,s_m),g(t_1,\ldots,t_n))$ with $f \neq g$ $\Rightarrow$ halt with failure.
     • $(f(s_1,\ldots,s_n),f(t_1,\ldots,t_n))$ $\Rightarrow$ replace this equation by the set $\{\,s_1 = t_1,\ldots,s_n = t_n\,\}$.
2. Once $E = \{x_1 = r_1,\ldots,x_\ell = r_\ell\}$ and every equation in it is isolated, return the substitution $\{\,x_1 \mapsto r_1,\ldots,x_\ell \mapsto r_\ell\,\}$.

Examples

Try running the algorithm on:

• $\{\,h\big(g(f(x),a)\big) = h\big(g(y,y)\big)\,\}$
• $\{\,h(f(y),y,f(z)) = h(z,f(x),x)\,\}$
• $\{\,h\big(g(f(x),z)\big) = h\big(g(y,y)\big)\,\}$

Properties

Theorem. Suppose we run the algorithm on $s = t$.

• If $s$ and $t$ are unifiable, the algorithm terminates and outputs a most general unifier of $s$ and $t$.
• If $s$ and $t$ are not unifiable, the algorithm terminates with failure.

We often write $\operatorname{mgu}(s,t)$ for a most general unifier and $\operatorname{mgs}(E)$ for a most general solution of the equation set $E$.

Exercise

Consider the trivial systems of equations $\varnothing$ and $\{a = a\}$.

• What is the set of all solutions?
• What is the set of most general solutions?

Revisiting the Ingredients of Lifting

• Lift the ordering $\succ$.
• Lift the selection function $\sigma$.
• Lift the calculus $\mathbb{S}\mathrm{up}^{\mathrm{sat}}$ (thanks to the lifting lemmas).

Most importantly, lifting works because we use most general unifiers.