Lecture 5: Term Orderings

Laura Kovács

Simple Ground Superposition Inference System

Superposition: (right and left)

$$\displaystyle \frac{{\color{red}l=r} \lor C \;\;\; {\color{red}s[l] = t} \lor D}{s[r]=t \lor C \lor D}(Sup),\;\;\;\;\;\; \frac{{\color{red}l=r} \lor C \;\;\; {\color{red}s[l]\neq t} \lor D}{s[r] \neq t \lor C \lor D}(Sup),$$

Equality Resolution:

$$\displaystyle \frac{{\color{red}s\neq s} \lor C}{C}(ER),$$

Equality Factoring:

$$\displaystyle \frac{{\color{red}s=t} \lor {\color{red}s=t'} \lor C}{s=t \lor t \neq t' \lor C}(EF),$$

Can this system be used for efficient theorem proving?

Not really. It has too many inferences. For example, from the clause $f(a) = a$ we can derive any clause of the form

$$f^m(a) = f^n(a)$$

where $m, n \geq 0$. Worst of all, the derived clauses can be much larger than the original clause $f(a) = a$.

The recipe is to use the previously introduced ingredients:

1. Ordering;
2. Literal selection;
3. Redundancy elimination.

Atom and literal orderings on equalities

Equality atom comparison treats an equality $s = t$ as the multiset $\dot{\{}s, t\dot{\}}$.

• $(s'=t')\succ_\text{lit} (s=t)$ if $\dot{\{} s',t' \dot{\}} \succ \dot{\{} s,t \dot{\}}$
• $(s'\neq t')\succ_\text{lit} (s\neq t)$ if $\dot{\{} s',t' \dot{\}} \succ \dot{\{} s,t \dot{\}} \\$ with $\succ_\text{lit}$ being an induced ordering on literals.

Ground Superposition Inference System $\mathbb{S}up_{\succ,\sigma}$

Let $\sigma$ be a well-behaved literal selection function.

Superposition: (right and left)

$$\displaystyle \frac{{\color{red}{\underline{l=r}}} \lor C \;\;\; {\color{red}{\underline{s[l] = t}}} \lor D}{s[r]=t \lor C \lor D}(Sup),\;\;\;\;\;\; \frac{{\color{red}{\underline{l=r}}} \lor C \;\;\; {\color{red}{\underline{s[l]\neq t}}} \lor D}{s[r] \neq t \lor C \lor D}(Sup),$$

where

$$\begin{array}{ll} 1 & l\succ r \\ 2 & s[l]\succ t \\ 3 & l=r \text{ is strictly greater than any literal in } C,\\ 4 & \text{(only for the superposition-right rule) } s[l]=t \text{ is greater than or equal to any literal in} D. \end{array}$$

Equality Resolution:

$$\displaystyle \frac{{\color{red}{\underline{s\neq s}}} \lor C}{C}(ER),$$

Equality Factoring:

$$\displaystyle \frac{{\color{red}{\underline{s=t}}} \lor {\color{red}s=t'} \lor C}{s=t \lor t \neq t' \lor C}(EF),$$

where

$$\begin{array}{ll} 1 & s\succ t \succeq t' \\ 2 & s=t \text{ is strictly greater than any literal in } C. \end{array}$$

Extension to arbitrary (non-equality) literals

• Consider a two-sorted logic in which equality is the only predicate symbol.
• Interpret terms as terms of the first sort and non-equality atoms as terms of the second sort.
• Add a constant $\top$ of the second sort.
• Replace non-equality atoms $p(t_1 , \ldots , t_n)$ by equalities of the second sort $p(t_1, \ldots, t_n) = \top$.

For example, the clause

$$p(a,b) \lor \neg q(a) \lor a\neq b$$

becomes

$$p(a,b) = \top \lor q(a) \neq \top \lor a\neq b$$

Binary resolution inferences can be represented by inferences in the superposition system

We ignore selection functions.

$$\displaystyle\frac{A\lor C_1 \;\;\; \neg A \lor C_2}{C_1 \lor C_2}(BR)$$ $$\displaystyle\frac { A=\top\lor C_1 \;\;\; A\neq \top \lor C_2 } { \displaystyle\frac{\top \neq \top \lor C_1 \lor C_2} {C_1 \lor C_2} (ER) } (Sup)$$

Exercise

Positive factoring can also be represented by inferences in the superposition system.

Simplification Ordering

When we deal with equality, we need to work with term orderings.

Consider a strict ordering $\succ$ on signature symbols, such that $\succ$ is well-founded.

The ordering $\succ$ on terms is called a simplification ordering if

1. $\succ$ is well-founded;
2. $\succ$ is monotonic: if $l \succ r$ , then $s[l] \succ s[r]$;
3. $\succ$ is stable under substitutions: if $l\succ r$ , then $l\theta \succ r\theta$.

One can combine the last two properties into one:

2a. If $l \succ r$ , then $s[l\theta] \succ s[r\theta]$.

A General Property of Term Orderings

If $\succ$ is a simplification ordering, then for every term $t[s]$ and its proper subterm $s$ we have $s \nsucc t[s]$. Why?

Consider an example.

$$\begin{array}{ll} f(a)=a\\ f(f(a))=a\\ f(f(f(a)))=a \end{array}$$

Then both $f(f(a))=a$ and $f(f(f(a)))=a$ are redundant. $\\$ The clause $f(a)=a$ is a logical consequence of $\{f(f(a))=a,\; f(f(f(a)))=a\}$; but is not redundant.

Exercise: Show that $\{f(a)=a,\;\; f(f(f(a)))\neq a\}$ is unsatisfiable, by using superposition with redundancy elimination.

How to “come up” with simplification orderings?

Term Algebra

Term algebra $TA(\Sigma)$ of signature $\Sigma$ :

• Domain: the set of all ground terms of $\Sigma$ .
• Interpretation of any function symbol $f$ or constant $c$ is defined as:

$$\begin{array}{rcl} f_{TA(\Sigma)}(t_1,\ldots,t_n) & \overset{\text{def}}{\Leftrightarrow} & f(t_1,\ldots,t_n);\\ C_{TA(\Sigma)} & \overset{\text{def}}{\Leftrightarrow} & C. \end{array}$$

Knuth-Bendix Ordering (KBO), Ground Case

Let us fix

• Signature $\Sigma$ , it induces the term algebra $TA(\Sigma)$.
• Total ordering $\gg$ on $\Sigma$, called precedence relation;
• Weight function $w : \Sigma \rightarrow \mathbb{N}$.

Weight of a ground term $t$ is

$$|g(t_1, \ldots, t_n)| = w(g) + \sum_{i=1}^n |t_i|$$

$g(t_1, \ldots, t_n) \succ_\text{KB} h(s_1, \ldots, s_m)$ if

1. $|g(t_1, \ldots, t_n)| \gt |h(s_1, \ldots, s_m)|$ (by weight) or

2. $|g(t_1, \ldots, t_n)| = |h(s_1, \ldots, s_m)|$ and one of the following holds:

   • 2.1 $g \gg h$ (by precedence) or
   • 2.2 $g = h$ and for some $1 \leq i \leq n$ we have $t_1 = s_1, \ldots, t_{i−1} = s_{i−1}$ and $t_i \succ_\text{KB} s_i$ (lexicographically).

Example

$$\begin{array}{ll} w(a) = 1\\ w(b) = 2\\ w(f) = 3\\ w(g) = 0 \end{array}$$ $$|f(g(a), f(a, b))| = |3(0(1), 3(1, 2))| = 3 + 0 + 1 + 3 + 1 + 2 = 10$$

The Knuth-Bendix ordering is the main ordering used in Vampire and all other resolution and superposition theorem provers.

Knuth-Bendix Ordering (KBO), Ground Case: Summary

Let us fix

• Signature $\Sigma$ , it induces the term algebra $TA(\Sigma)$.
• Total ordering $\gg$ on $\Sigma$, called precedence relation;
• Weight function $w : \Sigma \rightarrow \mathbb{N}$.

Weight of a ground term $t$ is

$$|g(t_1, \ldots, t_n)| = w(g) + \sum_{i=1}^n |t_i|$$

$g(t_1, \ldots, t_n) \succ_\text{KB} h(s_1, \ldots, s_m)$ if

1. $|g(t_1, \ldots, t_n)| \gt |h(s_1, \ldots, s_m)|$ (by weight) or

2. $|g(t_1, \ldots, t_n)| = |h(s_1, \ldots, s_m)|$ and one of the following holds:

   • 2.1 $g \gg h$ (by precedence) or
   • 2.2 $g = h$ and for some $1 \leq i \leq n$ we have $t_1 = s_1, \ldots, t_{i−1} = s_{i−1}$ and $t_i \succ_\text{KB} s_i$ (lexicographically).

• Note: Weight functions $w$ are not arbitrary functions.

  • need to be "compatible" with $\gg$.

• Why? Compare for example $a$ with $f(a)$ with arbitrary $\gg$ and $w$.

Weight Functions, Ground Case

A weight function $w : \Sigma \rightarrow \mathbb{N}$ is any function satisfying:

• $w(a) \gt 0$ for any constant $a \in \Sigma$;
• if $w(f) = 0$ for a unary function $f \in \Sigma$, then $f \gg g$ for all functions $g \in \Sigma$ with $f \neq g$. $\\$ That is, $f$ is the greatest element of $\Sigma$ wrt $\gg$.

As a consequence, there is at most one unary function $f$ with $w(f) = 0$.

Exercise

Consider a KBO ordering $\succ$ such that $inverse \gg times$ by precedence. Consider the literal:

$$inverse(times(x, y)) = times(inverse(y), inverse(x)).$$

Compare, w.r.t $\succ$, the left- and right-hand side terms of the equality when:

• $weight(inverse) = weight(times) = 1$;
• $weight(inverse) = 0$ and $weight(times) = 1$.

Same Property as for $\mathbb{BR}\sigma$

The conclusion is strictly smaller than the rightmost premise:

$$\displaystyle\frac{{\color{red}{\underline{l=r}}} \lor C \;\;\; {\color{red}{\underline{s[l]=t}}} \lor D}{s[r]=t\lor C \lor D}(Sup),\;\;\;\;\;\; \displaystyle\frac{{\color{red}{\underline{l=r}}} \lor C \;\;\; {\color{red}{\underline{s[l]\neq t}}} \lor D}{s[r]\neq t\lor C \lor D}(Sup),$$

where

1. $l \succ r$
2. $s[l] \succ t$,
3. $l = r$ is strictly greater than any literal in $C$,
4. $s[l] = t$ is greater than or equal to any literal in $D$.

New redundancy

Consider a superposition with a unit left premise:

$$\displaystyle\frac{\underline{l=r}\;\;\;\;\; \underline{s[l]=t} \lor D}{s[r]=t\lor D}(Sup),$$

Note that we have

$$l=r,\;\; s[r]=t\lor D {\color{red}{\models}} s[l]=t\lor D$$

and we have

$$s[l]=t\lor D {\color{red}{\succ}} s[r]=t \lor D$$

If we also have $s[l] = t \lor D \succ l = r$, then the second premise is redundant and can be removed.

This rule (superposition plus deletion) is sometimes called demodulation (also rewriting by unit equalities).

Exercise

Consider the KBO ordering ≻ generated by:

• the precedence $f \gg a \gg b \gg c$ $\\$ and
• the weight function $w$ with $w(f) = w(a) = w(b) = w(c) = 1$.

Consider the set $S$ of ground formulas:

$$\begin{array}{l} a=b\lor a=c\\ f(a) \neq f(b)\\ b=c \end{array}$$

Apply saturation on $S$ using an inference process based on the ground superposition calculus $\mathbb{S}up_{\succ,\sigma}$ (including the inference rules of ground binary resolution with selection).

Show that $S$ is unsatisfiable.

Challenge: Show that $S$ is unsatisfiable such that during saturation only 4 new clauses are generated.