Lecture 7: Non-Ground Superposition

Laura Kovács and Andrei Voronkov

Unification and Lifting (Recap)

Idea (Robinson 1965; Bachmair & Ganzinger 1990). Represent an infinite number of ground inferences by a single non-ground inference.

• For $\mathbb{BR}$ we work with non-ground clauses.
• We generalize “same” ground atom to unifiability of non-ground atoms.
• We compute only most general unifiers (mgus).

Lifting Lemma for $\mathbb{BR}$. Let $C$ and $D$ be clauses that share no variables. If there is a ground inference

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

then there exists a substitution $\sigma$ such that

$$\frac{C \qquad D}{C''}(\text{non-ground }\mathbb{BR})$$

and $C' = C''\sigma$.
Similar lifting lemmas hold for every inference in $\mathbb{BR}$ and $\mathbb{S}\mathrm{up}$.

What Should We Lift?

• Ordering $\succ$.
• Selection function $\sigma$.
• Calculus $\mathbb{S}\mathrm{up}^{\mathrm{sat}}$ (thanks to the lifting lemmas).

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

Knuth-Bendix Ordering (Ground Case Recap)

Fix a signature $\Sigma$, inducing the term algebra $\operatorname{TA}(\Sigma)$, together with:

• A total ordering $\gg$ on $\Sigma$ (the precedence);
• A weight function $w : \Sigma \to \mathbb{N}$.

For a ground term $t = g(t_1,\ldots,t_n)$ its weight is

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

The Knuth-Bendix ordering $\succ_\text{KB}$ compares ground terms as follows: $g(t_1,\ldots,t_n) \succ_\text{KB} h(s_1,\ldots,s_m)$ iff

1. $|g(t_1,\ldots,t_n)| > |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:
   • $g \gg h$ (by precedence);
   • $g = h$ and, for some $1 \leq i \leq n$, $t_1 = s_1,\ldots,t_{i-1} = s_{i-1}$ and $t_i \succ_\text{KB} s_i$ (lexicographically, left-to-right).

Note. Weight functions $w$ are not arbitrary—they must be compatible with $\gg$.

Weight Functions: Ground Case

A weight function $w : \Sigma \to \mathbb{N}$ satisfies:

• $w(a) > 0$ for every constant $a \in \Sigma$;
• If $w(f) = 0$ for a unary function $f \in \Sigma$, then $f \gg g$ for all $g \neq f$ (so $f$ is the greatest symbol in the precedence).

Weight Functions: Non-Ground Case

For non-ground terms extend $w$ to variables: $w : \Sigma \cup \mathrm{Vars} \to \mathbb{N}$, where $\mathrm{Vars}$ denotes the variables. We require:

• $w(x) = v_0$ for all variables $x$, with $v_0 > 0$;
• $w(a) \geq v_0$ for every constant $a \in \Sigma$;
• If $w(f) = 0$ for a unary function $f \in \Sigma$, then $f \gg g$ for all $g \neq f$.

Consequently, at most one unary function can have weight $0$. Given a term $s$ and variable $x$, we write $\#(x,s)$ for the number of occurrences of $x$ in $s$.

Knuth-Bendix Ordering (Non-Ground Case)

Let $w : \Sigma \cup \mathrm{Vars} \to \mathbb{N}$ be as above. For terms $s$ and $t$,

• $s \succ_\text{KB} t$ if $\#(x,s) \geq \#(x,t)$ for every variable $x$ and $|s| > |t|$ (by weight); or
• $\#(x,s) \geq \#(x,t)$ for every $x$, $|s| = |t|$, and one of the following holds:
  • $t = x$ and $s = f^n(x)$ for some $n \geq 1$;
  • $s = g(t_1,\ldots,t_n)$, $t = h(s_1,\ldots,s_m)$, and $g \gg h$ (by precedence);
  • $s = g(t_1,\ldots,t_n)$, $t = g(s_1,\ldots,s_n)$, 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).

Selection Functions and Lifting

If, for some grounding substitution $\theta$, the literal $L\theta$ is selected in $L\theta \lor C\theta$, then $L$ is selected in $L \lor C$.
Therefore, if the ground selection function is well-behaved, the lifted non-ground function is well-behaved as well.

Non-Ground Superposition

Superposition: $$\frac{\underline{l = r} \lor C \qquad \underline{s[l'] = t} \lor D}{(s[r] = t \lor C \lor D)\theta}(\text{Sup}), \qquad \frac{\underline{l = r} \lor C \qquad \underline{s[l'] \neq t} \lor D}{(s[r] \neq t \lor C \lor D)\theta}(\text{Sup}),$$

where

1. $\theta$ is an mgu of $l$ and $l'$;
2. $l'$ is not a variable;
3. $r\theta \not\succeq l\theta$;
4. $t\theta \not\succeq s[l']\theta$.

Observations.

• The ordering is partial, hence conditions such as $r\theta \not\succeq l\theta$.
• These conditions are checked a posteriori (after the rule fires); still, if $l \succ r$ then $l\theta \succ r\theta$, which helps prune some inferences a priori.

Equality Resolution and Equality Factoring

Equality Resolution. $$\frac{\underline{s \neq s'} \lor C}{C\theta}(\text{ER}),$$

where $\theta$ is an mgu of $s$ and $s'$.

Equality Factoring. $$\frac{\underline{l = r} \lor l' = r' \lor C}{(l = r \lor r \neq r' \lor C)\theta}(\text{EF}),$$

where $\theta$ is an mgu of $l$ and $l'$, $r\theta \not\succeq l\theta$, $r'\theta \not\succeq l\theta$, and $r'\theta \not\succeq r\theta$.

Non-Ground Binary Resolution

• Binary resolution: $$\frac{\underline{P} \lor C_1 \qquad \underline{\neg P'} \lor C_2}{(C_1 \lor C_2)\theta}(\text{BR}),$$ where $\theta$ is an mgu of $P$ and $P'$.
• Positive factoring: $$\frac{\underline{P} \lor \underline{P'} \lor C}{(P \lor C)\theta}(\text{Fact}),$$ where $\theta$ is an mgu of $P$ and $P'$.
• Negative factoring: $$\frac{\underline{\neg P} \lor \underline{\neg P'} \lor C}{(\neg P \lor C)\theta}(\text{Fact}),$$ where $\theta$ is an mgu of $P$ and $P'$.

🎬 Animation: Watch first-order resolution connect the mgu, selected literals, and resolvent.

Exercise

Consider the clause set

$$\begin{aligned} &\neg p(z,a) \lor \neg p(z,x) \lor \neg p(x,z),\\ &p(y,a) \lor p\big(y,f(y)\big),\\ &p(w,a) \lor p\big(f(w),w\big), \end{aligned}$$

where $p$ is a predicate, $f$ a function, $x,y,z,w$ variables, and $a$ a constant.

Give a refutation in the non-ground binary resolution system $\mathbb{BR}$. For every derived clause, specify the premises, the inference rule, and the mgu used.

Checking Redundancy

Assume the current search space $S$ contains no redundant clauses.
A redundant clause can appear only when a new child (the conclusion of an inference) is added.

We perform two kinds of redundancy checks after each inference under a fair strategy:

• The child itself is redundant.
• The child makes an existing clause redundant.

We use some fair strategy and perform these checks after every inference that generates a new clause.
In fact, one can do better in some of the cases.

Subsumption (Non-Ground)

A clause $C$ subsumes a clause $D$ if $C\theta \subseteq D$ for some substitution $\theta$.
Subsumption and Redundancy: If $S$ contains different clauses $C$ and $D$ such that $C$ subsumes $D$, then $D$ is redundant in $S$ and may be removed.

Exercise

Let $p$ be a unary predicate, $f$ a unary function, $x,y$ variables, and $c$ a constant.
Consider the clauses $C_1 = p(x) \lor p(y)$, $C_2 = p(x)$, and $D = p(f(c))$.

(a) Does $C_1$ subsume $D$?
(b) Does $C_2$ subsume $D$?

Demodulation (Non-Ground)

Demodulation replaces instances of equalities by simpler terms:

$$\frac{l = r \qquad L[l'] \lor D}{L[r\theta] \lor D}(\text{Dem}),$$

where $l\theta = l'$, $l\theta \succ r\theta$, and $(L[l'] \lor D) \succ (l\theta = r\theta)$.
Equivalently,

$$\frac{l = r \qquad L[l\theta] \lor D}{L[r\theta] \lor D}(\text{Dem}),$$

with $l\theta \succ r\theta$ and $(L[l\theta] \lor D) \succ (l\theta = r\theta)$.

General Redundancy (Non-Ground)

A clause $D$ is redundant with respect to $C$ if $D^*$ is redundant with respect to $C^*$, where $D^*$ and $C^*$ are the sets of ground instances of $D$ and $C$.
It suffices to find a substitution $\theta$ such that, for any ground instance $D^*$ of $D$:

1. $D^* \succ C\theta$, and
2. $D^*$ is a logical consequence of $C\theta$.

Generating vs. Simplifying Inferences

An inference

$$\frac{C_1 \quad \ldots \quad C_n}{C}$$

is simplifying if at least one premise $C_i$ becomes redundant after $C$ is added; we say $C_i$ is simplified into $C$. Otherwise the inference is generating.

Note. Deciding whether an inference is simplifying is undecidable (and so are several related checks).

Key principles.

1. Apply simplifying inferences eagerly; apply generating inferences lazily.
2. Checking for simplifying inferences must pay off—in practice, it must be cheap.

Redundancy Checking Workflow

Whenever a new clause $C$ is added:

• Retention test: Is $C$ redundant?
• Forward simplification: Can $C$ be simplified using existing clauses?
• Backward simplification: Does $C$ simplify or eliminate older clauses?

Examples of Redundancy Tests

• Retention:
  • Tautology checking.
  • Subsumption.
• Simplification:
  • Demodulation (forward/backward).
  • Subsumption resolution: $$\frac{A \lor C \qquad \neg B \lor D}{D}(), \qquad \frac{\neg A \lor C \qquad B \lor D}{D}(),$$ whenever some substitution $\theta$ satisfies $A\theta \lor C\theta \subseteq B \lor D$.

Cost of Redundancy Criteria

• Tautology checking is based on congruence closure.
• Subsumption and subsumption resolution are NP-complete.

Observations

• There may be chains (repeated applications) of forward simplifications;
• after such a chain, another retention test should be run.
• Backward simplification is often expensive.
• In practice, the retention test may include extra heuristics which may sacrifice completeness (e.g., dropping overly heavy clauses).