5.1 The Original Definition of Demodulation
Given an
equality unit clause, or
equation,
\(l\simeq r\), and a clause
\(C[l\sigma ]\) containing as subterm an instance
\(l\sigma \) of the side
l of
\(l\simeq r\), Larry Wos called
\(C[r\sigma ]\) an
immediate modulant of
\(C[l\sigma ]\) [
188]. Then a
k-
modulant, for
\(k > 0\), is the result of
k such replacement steps, and a
modulant is any
k-modulant [
188]. As a clause has infinitely many modulants in general, but only finitely many
k-modulants for a fixed
k, Larry Wos defined
k-modulation as the generation of a resolvent of parents
\(C_k\) and
\(D_k\), where
\(C_k\) and
\(D_k\) are
k-modulants of clauses
C and
D [
188]. However, Larry Wos also defined
demodulation as replacement by a modulant, where each immediate modulant has strictly fewer symbols than its predecessor, and the final modulant has no immediate modulant with fewer symbols [
188]. Thus, we can formalize his rule as follows:
$$\begin{aligned} Demodulation :\ \ \ \begin{array}{c}{S\cup \{l\simeq r,\ C[l\sigma ]\}}\\ \hline \hline {S\cup \{l\simeq r,\ C[r\sigma ]\}}\end{array} \ \ \ {\parallel \! C[l\sigma ] \!\parallel }\ >\ {\parallel \! C[r\sigma ] \!\parallel }, \end{aligned}$$
where
\(l\simeq r\) is called
demodulant,
\(\parallel \! C\! \parallel \) is the number of symbols in
C, and demodulation is defined as performing only one equational replacement step, according to the standard style for replacement rules. Subsequently, and especially in implementations, the name
demodulator was also used in place of demodulant.
However, the intended notion of number of symbols was not made explicit. If a term is viewed as a string also parentheses contribute to the symbol count, whereas they do not if a term is viewed as a tree. Also, number of symbols is ambiguous with respect to how to count repeated occurrences of the same symbol.
The
size of an atom is the number of occurrences of predicate, function, constant, and variable symbols. For example,
\(\parallel \! P(f(a),g(a))\!\parallel \ = 5\). Assume that the number of symbols in a clause is defined as the sum of the sizes of the atoms that occur in the clause. Then, the ordering whereby
C is smaller than
D if
\(\parallel \! C\!\parallel \ <\ \parallel \! D\!\parallel \) is well-founded. The ordering based on size was implemented in
Otter, and remained available alongside with more sophisticated orderings such as
recursive path orderings [
74] and
Knuth-Bendix orderings [
107] that were introduced later (cf. Sect.
4.2). Since there are infinitely many variants of a clause and they all have the same size, variants have to be eliminated by subsumption (cf. Sect.
2.2). Indeed, theorem provers such as
Otter apply subsumption
before demodulation, so that if two clauses are variants, one is deleted by subsumption.
Nonetheless, the size-based ordering does not allow the system to apply as demodulants many equations that it would be useful to apply, because the two sides of the equation have the same number of symbols. Also, this ordering may not allow the system to apply an equation in the desired direction. For example, \(\parallel \! x * (y + z) \!\parallel \ = 5\) and \(\parallel \! x * y + x * z \!\parallel \ = 7\), so that the distributivity law \(x * (y + z) \simeq x * y + x * z\) would be applied from right to left.
In summary, Larry Wos’ definition of demodulation is well-founded, but the problem of well-founded demodulation, in the sense of finding more and better well-founded orderings to enable the demodulation of clauses, remained open.
5.2 Well-Founded Demodulation by Rewrite Rules
The discovery of a solution to the problem of well-founded demodulation was advanced significantly in the context of the
Knuth–Bendix completion procedure [
101,
107]. This procedure works with
rewrite rules, where a rewrite rule is an equation
\(l\simeq r\) that is written
\(l\rightarrow r\) because
\(l\succ r\) in a well-founded ordering
\(\succ \) on terms. A rewrite rule
reduces or
rewrites a term
\(t[l\sigma ]_u\) to
\(t[r\sigma ]_u\), where
\(\sigma \) is a substitution, the notation
\(t[l\sigma ]_u\) means that
\(l\sigma \) occurs as a subterm in
t at position
u, and
\(t[r\sigma ]_u\) is the term obtained by replacing the occurrence of
\(l\sigma \) at position
u with
\(r\sigma \). Positions are strings of natural numbers: if terms are viewed as trees and arcs are labeled with natural numbers, every subterm has a position defined as the string of natural numbers from the root to the subterm. From now on positions are omitted for simplicity.
Knuth and Bendix defined a well-founded ordering on terms, called since then the
Knuth–Bendix ordering or KBO for short [
107,
121,
124]. A KBO orders terms based on a
precedence and a
weighting function. A precedence is an ordering on symbols that may be partial or total. A weighting function assigns non-negative weights to symbols. Since the definition is parametric with respect to precedence and weighting function, it defines a family of orderings.
A KBO is a
reduction ordering, meaning that it is well-founded,
stable (
\(t \succ u\) implies
\(t\sigma \succ u\sigma \) for all substitutions
\(\sigma \)), and
monotonic (
\(t \succ u\) implies
\(c[t] \succ c[u]\) for all contexts
c, where a context is a term with a hole). Another reduction ordering is the
recursive path ordering [
74], or RPO for short, that orders terms based on a
precedence and a
status (either multiset [
74] or lexicographic [
106]) of every symbol. If the status is lexicographic for all symbols, the ordering is called
lexicographic path ordering, or LPO for short. Here too, since the definitions are parametric with respect to precedence and status, one gets families of orderings. The interested reader may find more information about orderings in surveys on rewriting [
75,
76,
78]. Since weights are non-negative, KBO’s correlate well with size, and therefore incorporate the intuition in Larry Wos’ definition of demodulation, whereby clauses are made simpler by reducing the number of symbols.
The Knuth–Bendix completion procedure was formalized as an inference system [
6‐
8] that transforms pairs (
E;
R), where
E is a set of equations, and
R is a set of rewrite rules, such that for all rules
\(l\rightarrow r\in R\) it holds that
\(l\succ r\) in a given reduction ordering
\(\succ \) on terms. The inference rules of completion are seen as transforming the equational proofs of the theorems in
\(Th(E \cup R)\) with respect to a
proof ordering, that is, a stable, monotonic (with respect to replacement of subproofs), and well-founded ordering > on proofs [
6‐
8,
49]. A key property of completion is that the inference rules are
proof-reducing [
54] or
good [
49]: an inference rule deriving
\((E^\prime ;R^\prime )\) from (
E;
R) is
good, if for all theorems
\(s\simeq t\in Th(E \cup R)\) and for all proofs
\(\pi \) of
\(s\simeq t\) in
\(E \cup R\) there exists a proof
\(\pi ^\prime \) of
\(s\simeq t\) in
\(E^\prime \cup R^\prime \) such that
\(\pi \ge \pi ^\prime \).
Since the state of the derivation is a pair (
E;
R), there are three contraction inference rules that realize well-founded demodulation by reducing a side of an equation or a side of a rewrite rule.
Simplify reduces a side of an equation:
$$\begin{aligned} Simplify :\ \ \ \begin{array}{c}{(E\cup \{p[l\sigma ] \simeq q\};R\cup \{l \rightarrow r\})}\\ \hline \hline {(E\cup \{p[r\sigma ] \simeq q\};R\cup \{l \rightarrow r\})}\end{array} \end{aligned}$$
where
\(\simeq \) is symmetric.
Compose reduces the right-hand side of a rewrite rule, so that another rewrite rule is produced:
$$\begin{aligned} Compose :\ \ \ \begin{array}{c}{(E;R\cup \{p \rightarrow q[l\sigma ], l \rightarrow r\})}\\ \hline \hline {(E;R\cup \{p \rightarrow q[r\sigma ],\ l \rightarrow r\})}\end{array} \end{aligned}$$
Collapse reduces the left-hand side of a rewrite rule, so that an equation is produced:
where
is the strict
encompassment ordering on terms. If an equation in
E has the form
\(s \simeq s\), the
Delete inference rule removes it. If an equation
\(p\simeq q\) in
E is such that
\(p\succ q\), the
Orient inference rule removes
\(p\simeq q\) from
E and adds
\(p\rightarrow q\) to
R.
The
encompassment ordering is obtained by combining the
subterm ordering and the
subsumption ordering on terms. The subterm ordering is defined by
\(t \unlhd s\) if
\(s = c[t]\) for some context
c. The subsumption ordering on terms is defined by
\(s{\mathop {\_\!\_}\limits ^{\lessdot }}t\) if
\(t = s\vartheta \) for some substitution
\(\vartheta \). Terms
s and
t are variants, written
\(s\doteq t\), if
\(s {\mathop {\_\!\_}\limits ^{\lessdot }}t\) and
\(t {\mathop {\_\!\_}\limits ^{\lessdot }}s\). The encompassment ordering is defined by
if
\(t = c[s\vartheta ]\) for some context
c and substitution
\(\vartheta \). The strict encompassment ordering is defined by
if
and
, that is,
\(t = c[s\vartheta ]\) where either the context
c is not empty or the substitution
\(\vartheta \) is not a variable renaming.
The purpose of the strict encompassment condition of the
Collapse inference rule is to prevent
\(l\rightarrow r\) from reducing
\(p[l\sigma ]\) if
l and
\(p[l\sigma ]\) are variants. The reason is that such a step is not good (in the above sense of proof-reducing) [
6‐
8]. In the Knuth–Bendix procedure the co-existence of two rewrite rules whose left-hand sides are variants is avoided by giving
Simplification higher priority than
Orient. If
\(p\simeq q\) and
\(l\simeq r\) are two equations such that
\(p\succ q\),
\(l\succ r\), and
\(p \doteq l\), one of them, say
\(p\simeq q\), gets oriented first into
\(p\rightarrow q\), so that
\(p\rightarrow q\) simplifies
\(l\simeq r\) to
\(q\simeq r\) before \(l\simeq r\) may get oriented into
\(l\rightarrow r\).
If an equation in E can be neither simplified, nor deleted, nor oriented, the procedure fails. Thus, Knuth-Bendix completion provided only a partial solution to the problem of well-founded demodulation.
5.3 Well-Founded Demodulation by Equations
Knuth–Bendix completion solved the problem of well-founded demodulation at the price of considering as demodulants only those equations that can be oriented into rewrite rules by the adopted ordering. This limitation was removed with the inception of
unfailing [
98] or
ordered [
6,
7,
9] completion, henceforth completion for short. Completion allows the inference system to use equations as demodulants provided the applied instance is oriented by the ordering.
Completion is a theorem-proving strategy for problems of the form
\(E \models ^? \forall {\bar{x}}. s\simeq t\), where
E is a set of equations, the presentation of an equational theory, and
\({\bar{x}}\) is the vector of all variables in
\(s\simeq t\) [
9,
42,
52,
54,
98,
101]. The negation of the conjecture yields
\({\hat{s}}\not \simeq {\hat{t}}\), where
\({\hat{s}}\) and
\({\hat{t}}\) are
s and
t, respectively, with all the variables in
\({\bar{x}}\) replaced by Skolem constants. The given ordering
\(\succ \) on terms is assumed to be a reduction ordering [
6,
7,
9], or a
complete simplification ordering (CSO) [
98]. A simplification ordering is stable, monotonic, and with the
subterm property, which means that it includes the strict subterm ordering (i.e.,
\(p\rhd l\) implies
\(p\succ l\)). A simplification ordering is well-founded [
74], hence it is a reduction ordering. A complete simplification ordering is also total on ground terms. KBO’s, RPO’s, and LPO’s are simplification orderings. KBO’s and LPO’s are CSO’s if the precedence is total, but not all RPO’s are CSO’s [
10].
As it is no longer necessary to separate equations and rewrite rules, and completion is seen as theorem proving, the inference system can be written [
42,
52,
54] as transforming pairs
\((E;{\hat{s}}\not \simeq {\hat{t}})\), where
\({\hat{s}}\not \simeq {\hat{t}}\) is called the
target. The inference rules of completion are good [
49] or proof-reducing [
42,
54] with respect to all ground theorems, which is enough for theorem proving, since the target is ground. The objective of the derivation is to reduce
\({\hat{s}} \) and
\({\hat{t}}\) to a common form so as to discover a contradiction with
\(x\simeq x\), the clausal form of the reflexivity axiom for equality. Accordingly, one can distinguish between
Simplification of the target:
$$\begin{aligned} \begin{array}{c}{(E\cup \{l \simeq r\};{\hat{s}}[l\sigma ]\not \simeq {\hat{t}})}\\ \hline \hline {(E\cup \{l \simeq r\};{\hat{s}}[r\sigma ]\not \simeq {\hat{t}})}\end{array} \ \ \ l\sigma \succ r\sigma , \end{aligned}$$
and
Simplification of the presentation:
where
\(l \simeq r\) is called a
simplifier, and the second condition incorporates the side condition of
Collapse. This side condition for simplification lets
\(l \simeq r\) simplify
\(p[l\sigma ] \simeq q\) when
\(p[l\sigma ]\) is a variant of
l, but
q is not a variant of
r, provided that
\(q\succ p[r\sigma ]\), or, equivalently,
\(q\succ r\sigma \) (if
\(p[l\sigma ]\doteq l\), the context
p is empty,
\(\sigma \) is a variable renaming,
\(p[l\sigma ] = l\sigma \), and
\(p[r\sigma ] = r\sigma \)). For example, simplifying
\(f(e,x)\simeq x\) by
\(f(e,y)\simeq y\) is not allowed; simplifying
\(f(e,x)\simeq h(x)\) by
\(f(e,y)\simeq y\) is allowed as
\(h(x)\succ x\); simplifying
\(f(e,y)\simeq y\) by
\(f(e,x)\simeq h(x)\) is not allowed as
\(y\not \succ h(y)\).
The next challenge was to generalize simplification to clauses, as intended in Larry Wos’ definition of demodulation, while preserving as much as possible the behavior of simplification in completion. This requires to extend the ordering
\(\succ \) beyond terms. A step in this direction was achieved with the inference system in [
155]. This system assumes that the ordering
\(\succ \) is a CSO on terms and atoms that satisfies two additional properties. First, for all terms
l,
r,
p, and
q, such that
\(l\succeq r\), and for all atoms
A, (i) if
\(l\unlhd A\) and the predicate symbol of
A is not
\(\simeq \), then
\((l\simeq r) \prec A\); and (ii) if
\(l\lhd p\) or
\(l\lhd q\), then
\((l\simeq r) \prec (p\simeq q)\). Second, for all ground terms
l,
r, and
s, and for all ground atoms
A, if
\(l\succ r\),
\(l\succ s\), and
\((l\simeq r) \prec A \prec (l\simeq s)\), then
A has the form
\(l\simeq t\) for some ground term
t.
This definition is illustrated in [
155] with a predicate-first extension of a CSO
\(\succ \) on terms to atoms. It assumes a total precedence on predicate symbols such that
\(\simeq \) is the smallest predicate symbol. Then,
\(P(s_1,\ldots ,s_m) \prec Q(t_1,\ldots ,t_n)\) holds if
P is smaller than
Q in the precedence, or
\(P = Q \ne {{\simeq }}\) and
\((s_1,\ldots ,s_m) \prec _{lex} (t_1,\ldots ,t_n)\), or
\(P = Q = {{\simeq }}\) and
\((s_1,s_2) \prec _{mul} (t_1,t_2)\), where
\(\prec _{lex}\) and
\(\prec _{mul}\) are the lexicographc and multiset extensions of
\(\prec \), respectively.
The inference system in [
155] includes a simplification inference rule that allows a simplifier
\(l \simeq r\) to simplify a clause
\(C[l\sigma ]\) to
\(C[r\sigma ]\), if
\(l\sigma \succ r\sigma \) and
\(C[l\sigma ]\) contains an atom
A such that
\(A\succ (l\sigma \simeq r\sigma )\). While the simplification rule of [
155] allows some simplification, it does not preserve the behavior of simplification in completion.
The footnote on page 2 of [
10] says
^{1} that the method of [
155] “does discuss simplification to some extent, but for practical purposes his simplification tecniques are inadequate even for the very simplest case – completion of sets of universally quantified equations.” The issue is the generalization of the ordering beyond terms. The inference system of the
superposition calculus [
10]—henceforth
\(\mathcal{SP}\mathcal{}\)—offered a solution with a systematic way to extend a reduction ordering on terms to atoms, literals, and clauses. The reduction ordering is assumed to be complete or
completable, which means it is included in a complete ordering. All RPO’s are completable [
10]. The first step is to treat non-equational literals as equational literals by treating non-equational atoms like terms, and reading a positive literal
L as
\(L\simeq \top \) and a negative literal
\(\lnot L\) as
\(L\not \simeq \top \), where
\(\top \) is a new symbol such that
\(t \succ \top \) for all terms
t.
The second step is to extend the ordering \(\succ \) on terms to literals. This can be done in one of two ways. One way is to treat an equation \(p\simeq q\) as the multiset \(\{p, q\}\), a negated equation \(p\not \simeq q\) as the multiset \(\{p, p, q, q\}\), and compare literals in the multiset extension of the ordering on terms. The other one is to treat an equation \(p\simeq q\) as the multiset of multisets \(\{\{p\}, \{q\}\}\), a negated equation \(p\not \simeq q\) as the multiset of multisets \(\{\{p, \bot \}, \{q, \bot \}\}\), where \(\bot \) is a new symbol such that \(t \succ \bot \succ \top \) for all terms t, and compare literals by taking twice the multiset extension of the ordering on terms. The third step is to extend the ordering on literals to clauses by taking once more the multiset extension.
Simplification appears in
\(\mathcal{SP}\mathcal{}\) as an instance of an inference rule called
contextual reductive rewriting [
10]. If the simplifier is a unit equational clause, contextual reductive rewriting yields the following rule:
$$\begin{aligned} Simplification :\ \ \ \begin{array}{c}{S\cup \{C[l\sigma ],\ l \simeq r\}}\\ \hline \hline {S\cup \{C[r\sigma ],\ l \simeq r\}}\end{array} \ \ \ \begin{array}{ccc} l\sigma \succ r\sigma ,&\,&C[l\sigma ]\succ (l\sigma \simeq r\sigma ).\end{array} \end{aligned}$$
The second side condition requires that the applied instance of the simplifier is smaller than the clause it simplifies. This condition is only superficially similar to the one of the simplification rule in [
155] as the difference is in the ordering.
However, Simplification of \(\mathcal{SP}\mathcal{}\) and Simplification of completion do not behave in general in the same way in the purely equational case.
A comparison of the second condition for
Simplification in completion with the second condition for
Simplification of
\(\mathcal{SP}\mathcal{}\) explains the difference. Assume that the ordering on terms is a CSO. The second condition for
Simplification in completion is
. The second condition for
Simplification in
\(\mathcal{SP}\mathcal{}\) when an equation
\(l\simeq r\) simplifies a unit positive equational clause
\(p[l\sigma ] \simeq q\) is
\(\{p[l\sigma ], q\}\succ _{mul} \{l\sigma , r\sigma \}\).
If the
Simplification rule of completion applies because
holds as
p is not empty, we have
\(p[l\sigma ] \succ l\sigma \succ r\sigma \) by the subterm property and the condition
\(l\sigma \succ r\sigma \) in both simplification rules. Thus,
\(\{p[l\sigma ], q\}\succ _{mul} \{l\sigma , r\sigma \}\) follows and
Simplification of
\(\mathcal{SP}\mathcal{}\) applies.
If the
Simplification rule of completion applies because
does not hold (
p is empty and
\(\sigma \) is a variable renaming) and
\(q \succ p[r\sigma ]\) holds, we have
\(p[l\sigma ] = l\sigma \),
\(p[r\sigma ] = r\sigma \), and hence
\(q \succ r\sigma \), so that
\(\{p[l\sigma ], q\}\succ _{mul} \{l\sigma , r\sigma \}\) follows and
Simplification of
\(\mathcal{SP}\mathcal{}\) applies.
If the
Simplification rule of completion applies because
holds as
p is empty, but
\(\sigma \) is not a variable renaming, and
\(q \succ p[r\sigma ]\) does not hold, then
\(\{p[l\sigma ], q\}\succ _{mul} \{l\sigma , r\sigma \}\) does not follow, and
Simplification of
\(\mathcal{SP}\mathcal{}\) does not apply. Example
4 illustrates this situation, where completion lets a simplifier (i.e.,
\(f(x) \rightarrow b\)) rewrite a proper instance of its left-hand side (i.e.,
f(
b)) even if the right-hand side of the simplifier (i.e.,
b) is larger than the right-hand side of the rewrite rule to be simplified (i.e.,
c).
It is also interesting to see how simplification is implemented. For instance, the
E prover [
157] distinguishes between
Simplification of negative literals and
Simplification of positive literals. The former is
$$\begin{aligned} \begin{array}{c}{S\cup \{p[l\sigma ] \not \simeq q \vee D,\ l \simeq r\}}\\ \hline \hline {S\cup \{p[r\sigma ] \not \simeq q \vee D,\ l \simeq r\}}\end{array} \ \ \ l\sigma \succ r\sigma , \end{aligned}$$
because
\(l\sigma \succ r\sigma \) implies
\(\{p[l\sigma ], p[l\sigma ], q, q\}\succ _{mul} \{l\sigma , r\sigma \}\). Indeed, if
p is not empty,
\(\{p[l\sigma ], p[l\sigma ], q, q\}\succ _{mul} \{l\sigma , r\sigma \}\) follows from
\(p[l\sigma ] \succ l\sigma \succ r\sigma \) as discussed above. If
p is empty,
\(\{l\sigma , l\sigma , q, q\}\succ _{mul} \{l\sigma , r\sigma \}\) follows from
\(l\sigma \succ r\sigma \). Thus, it suffices to consider the literal being rewritten to establish the second condition of
Simplification of
\(\mathcal{SP}\mathcal{}\). On the other hand,
Simplification of positive literals embeds conditions from the inference rules of completion:
^{2}Consider the second condition. If the first disjunct is true, either
\(\{M, \top \} \succ _{mul} \{p[l\sigma ], q\}\) or
\(\{M, M, \top , \top \} \succ _{mul} \{p[l\sigma ], q\}\). Either way,
\(M\succ p[l\sigma ]\) and
\(M\succ q\), so that
\(M\succ p[l\sigma ] \succeq l\sigma \succ r\sigma \) holds. Thus, either
\(\{M, \top \} \succ _{mul} \{l\sigma , r\sigma \}\) or
\(\{M, M, \top , \top \} \succ _{mul} \{l\sigma , r\sigma \}\) holds and the second condition of
Simplification of
\(\mathcal{SP}\mathcal{}\) is fulfilled. If the second disjunct
\(p[l\sigma ] \not \succ q\) is true, the step is an instance of
Simplify or
Compose. If the third disjunct
is true, the step is an instance of
Collapse. Although the second disjunct
\(q \succ p[r\sigma ]\) in the second condition of
Simplification in completion does not appear, this confirms that the conditions for simplification from completion are important in the practice.
Larry Wos’ intuition of demodulation as comprising multiple steps, until no further step can be applied, was captured in the context of completion and rewriting with the notion of normalization, or reduction to normal form. A clause C is in normal form with respect to a set S of clauses, if no unit equational clause in S can simplify it; equivalently, C is irreducible with respect to S, or S-irreducible. The normal form of C with respect to S is denoted \(C\!\downarrow _S\), where \({C \downarrow _S}\ = C\) if C is S-irreducible.
5.4 Demodulation and the Given-Clause Algorithm
Larry Wos was interested in the application of demodulation in the context of the set-of-support strategy [
188], which leads to the more general issue of the application of demodulation in the given-clause algorithm. The goal is to ensure that the given-clause algorithm implements an
eager-contraction search plan, namely one where contraction has priority over expansion (e.g., [
56]). In other words, the objective is to prevent a clause that can be deleted or replaced from playing the role of parent in an expansion inference.
In the given-clause algorithm, when a new clause C is generated by expansion, C is subject to forward contraction, that is, contraction with respect to a set S of already existing clauses. The prover tries first the deletion rules. Thus, C may be deleted by tautology deletion, or by purity deletion, or by subsumption by a clause in S (forward subsumption), or because it is a unit equational clause \(s\simeq s\).
If clause
C survives these tests, the prover tries the replacement rules. Thus,
C may be simplified by clausal simplification by a clause in
S, or reduced to
\(C\!\downarrow _S\) by demodulation with the demodulants in
S. Let
\(C\!\downarrow _S\) represent the final result of the application of all applicable replacement rules. If
C, and hence
\(C\!\downarrow _S\), is an equation, the test to determine whether it can be oriented is applied to
\(C\!\downarrow _S\). Thus, the implementation of contraction respects the requirement from completion of orienting equations only after their sides have been normalized (cf. Sect.
4.2).
Only at this stage clause \(C\!\downarrow _S\) gets an identifier and is appended to the sos
list. Therefore, forward contraction is part of the generation of a new clause. Indeed, in Otter this phase is called preprocessing of a clause. Also the test for the generation of the empty clause happens during preprocessing: if \(C\!\downarrow _S\) is a unit clause the prover tests whether it generates the empty clause with a unit clause in usable
or sos
. This is because one wants to get the empty clause as soon as possible. Thus, the test for a contradiction is applied as soon as a unit clause is generated, without waiting until it is selected as given clause.
For backward contraction the prover tests whether \(C\!\downarrow _S\) can contract a previously existing clause \(D\in S\). In Otter this phase is called post-processing of a clause. For all \(D\in S\) for which this is the case, D is treated like if it were a newly generated clause, and subjected to forward contraction as described above. The resulting \(D\!\downarrow _S\) gets a new identifier and is appended to the sos
list. Thus, a clause generated by backward contraction is treated as a clause generated by expansion.
There are two versions of the given-clause algorithm, named from the
Otter prover [
127,
128] and the
E prover [
73,
157‐
159], respectively. The two versions differ primarily in the implementation of backward contraction. In both versions the set
S of clauses in the above description of forward contraction is given by
\(\mathtt {usable}\cup \mathtt {sos}\), meaning the union of the set of clauses in
usable
and the set of clauses in
sos
. On the other hand, the set
S of clauses in the above description of backward contraction is
\(\mathtt {usable}\cup \mathtt {sos}\) in the
Otter version, whereas it is
usable
in the
E version.
The
Otter version of the given-clause algorithm aims at maintaining the set
\(\mathtt {usable}\cup \mathtt {sos}\) inter-reduced or, more generally,
contracted [
49]. Suppose that the expansion inferences between a given clause
C and the clauses in
usable
generate a bunch of new clauses, each of whom is subjected to forward contraction as described above, so that clauses
\(C_0,\ldots ,C_k\) get appended to
sos
. In the
Otter version, the prover tests whether
\(C_i\), for all
i,
\(0\le i\le k\), can backward-contract any clause in
\(\mathtt {usable}\cup \mathtt {sos}\). Suppose that for all
i,
\(0\le i\le k\), backward-contraction by
\(C_i\) appends clauses
\(D^i_0,\ldots ,D^i_{n_i}\) to
sos
. Then, for all
i,
\(0\le i\le k\), for all
j,
\(0\le j\le n_i\), the prover tests whether
\(D_j\) can backward-contract any clause in
\(\mathtt {usable}\cup \mathtt {sos}\). The process continues until no more contraction applies.
The E version of the given-clause algorithm aims at maintaining usable
contracted. The prover tests whether a clause C can backward-contract any clause in usable
only when C is selected as given clause and moved from sos
to usable
. As usable
may have changed since the time when C was subjected to forward contraction, the prover first applies the clauses in usable
to contract C, and then applies C to contract the clauses in usable
, before trying the expansion inferences between C and clauses in usable
. If a clause in usable
is removed by backward contraction, its descendants in sos
are deleted as orphans. Except for orphan deletion, all backward contraction happens in usable
. The rationale is that maintaining usable
contracted is good enough, because the premises of expansion inferences come from usable
.
In the E version of the given-clause algorithm the lists usable
and sos
were renamed active
and passive
, respectively. The E version was born primarily from a concern that the cost of backward contraction as in the Otter version could outweight its benefits. For example, it may happen that the prover spends a lot of time doing backward contraction, when it would be more beneficial to go ahead with expansion, because an expansion inference with the next given clause would generate a unit clause that yields the contradiction. On the other hand, the delay in backward contraction in the E version may cause the passive
list to grow too much, reaching a memory limit, or it may delay finding a proof. For example, it may happen that the prover goes ahead to do more expansion, postponing backward demodulation steps in sos
that would generate a unit clause that yields the contradiction.
In practice, most clauses that get deleted are deleted by forward contraction. Then, expansion and backward demodulation can be seen as two ways to generate clauses that need to be balanced. One could say that the Otter version leans toward prioritizing backward demodulation and the E version leans toward prioritizing expansion. There is no conclusive evidence that one is better than the other in general. Most theorem provers feature both versions of the given-clause algorithm, because one pays off on some problems and the other on others.