Term orderings play a critical role in most modern automated theorem proving systems, in particular for systems dealing with equality. In this paper we report on a set of experiments with the superposition theorem prover E, comparing the performance of the system under Knuth-Bendix Ordering and Lexicographic Path Ordering with a number of diferent precedence and weight generation schemes. Results indicate that relative performance under a short time limit seems to be a good predictor for longer run times and that KBO generally outperforms LPO. Also, if other strategy elements (especially clause selection) are independent of the ordering, performance of a given ordering instance with one strategy is a decent predictor of performance with a diferent strategy.
The root cause of dificulty in automated theorem proving is the size of the search space,
i.e. the space of possible derivations. Many improvements in calculi have introduced ways
to reduce the branching factor of this search space, by identifying strictly unnecessary
inferences. One of the more important techniques in the context, in particular for
equational reasoning, is the use of term orderings, to break the symmetry of equality,
and also to impose additional constraints on possible inferences. This was pioneered
by Knuth and Bendix in their paper on completion [
When these theoretical results are translated to practical reasoning systems, there are additional challenges. Orderings need to be eficiently implemented, and they need to be instantiated for any given proof problem. Both the KBO and the LPO (Lexicographic Path Ordering), the two most frequently used orderings, are actually ordering schemata. In the concrete case, both need a symbol precedence. The KBO additionally needs an assignments of weights to function (and predicate) symbols.
While e.g. Otter [
Over time, the theorem prover E[
In this paper, we want to address a number of questions regarding the performance of these diferent schemes.
1. How do they compare for overall performance? 2. Does good performance of an ordering in one setting translate to diferent settings? In particular, if we replace only the ordering, can (relative) performance be extrapolated from one search strategy to another? 3. Similarly, can (relative) performance be extrapolated from shorter to longer run times?
Most of our experiments were done only on unit-equational examples, where the influence
of the term ordering is more important. However, we have also ran one experiment on all
usable TPTP [
Finally, most theorem provers we are aware of implement rewriting with unorientable unit equations in a way that is strictly weaker than supported by theory. In E, we have introduced rewriting with strong instances, a technique that often allows for more simplification than these conventional implementations. We also analyse the data with respect to this new technique.
We start the paper with a short definition of the most important terms and concepts, including the idea of rewriting with strong instances. In the next section, we discuss the experimental setting, including the diferent ordering generation schemes and applications to simplification. In the experimental section, we discuss the primary results. Finally, we mention some related and future work, and conclude.
(SP)
C ∨ s ' t D ∨ u 6' v (C ∨ D ∨ u[p ← t] 6' v)σ (RP)
s ' t s ' t
u ' v ∨ C u[p ← tσ] ' v ∨ C if if • u|p is not a Variable, σ = mgu(u|p, s) • sσ 6< tσ, uσ 6< vσ • (s ' t)σ is strictly maximal in (C ∨ s ' t)σ • (u 6' v)σ is maximal in (D ∨ u 6' v)σ • u|p = sσ, sσ > tσ • u ' v is not maximal or u 6> v or u|p 6= u Note that the double line in (RP) denotes a simplification rule, i.e. a rule in which the premises are replaced by the results.
We assume the standard first-order notions of a signature, consisting of function symbols with associated arities, and variable symbols. Terms are either variables, or are constructed from a function symbol with the proper number of arguments. Constants are a special case of function symbols with arity zero (and hence a constant is a term). Terms without variables are called ground terms. Equations are unordered pairs of terms, literals are either equations or negated equations, and clauses are multi-sets of literals1 interpreted (and written) as disjunctions. Substitutions replace variables by terms and can be applied to variables, terms, literals and clauses. We use s, t, u, v to denote terms, C, D to denote (partial) clauses, and σ for substitutions. We use t|p to denote the subterm of t at position p and t[p ← s] for term t with the subterm at position p replaced by s.
Saturating theorem provers try to show that a set of clauses is unsatisfiable by the process of saturation, i.e. by using inference rules to derive new clauses from existing clauses with the aim of eventually producing the empty clause. The proof search is usually organised by some variant of the given-clause-algorithm. This algorithm maintains the proof state in the form of two separate sets of clauses. The set P of processed clauses is initially empty. The set U of unprocessed clauses initially contains all clauses of the proof problem. The algorithm repeatedly selects a given clause g from U and performs all inferences in which g is one premise and all other premises are from P . The given clause is then moved into P , the resulting new clauses into U . The algorithm terminates if the empty clause is derived (representing a proof that the original clause set is unsatisfiable), or if the set U runs empty (in which case the proof search fails). In addition to this basic operations, a significant proportion of time is spent on simplification , removing redundant clauses and replacing clauses with, in a certain sense, smaller and simpler clauses. The selection of the given clause has to be fair (i.e. no clause can be delayed infinitely long), and is also one of the most important heuristic choice points for the proof search.
The most important inference in modern calculi is superposition, a restricted version
of paramodulation. A paramodulation inference has two premises: the main premise, an
1Non-equational literals can be encoded as equations with a reserved constant > with a separate Boolean
sort.
instance of which forms the core of the newly inferred clause, and a side premise, which
contains at least one positive equational literal and is used as a (lazy) conditional rewrite
rule to modify the instance of the main premise. To perform an inference, one side of
a positive literal of the side premise is overlapped into a subterm of the main premise,
followed by instantiation and replacement of the overlapped term by the instance of the
other side of the inference literal in the side premise. The instances of other literals
of the side premise are inherited by the newly generated child clause. Paramodulation
inferences can be restricted in certain ways. In particular, we can use a simplification
ordering on terms, lift it to literals, and restrict inferences to maximal literals. In this
case, we call such an inference a superposition inference. Fig 1 shows the inference rule
(SP) for superpositions into a positive literal. Term orderings also allow us to use strictly
decreasing instances of positive unit clauses for simplification (i.e. destructive rewriting,
in which a parent clause is replaced by the result). Rule RP in figure 1 describes rewriting
of a positive literals. Both rules have very similar counterparts for overlapping into or
rewriting negative literals. See e.g. [
As described above, the two most frequently used classes of orderings are the KBO [
The KBO requires a weight assignment to function symbols, and a precedence on these symbols. It compares terms first by weight (i.e. numerical comparison of the summed weight of all symbols in the term), breaking ties by top symbol (using the precedence), and further breaking ties by lexicographic comparison of subterms. It additionally requires each variable to occur in the smaller term no more often than in the larger term.
The LPO requires only a precedence on function symbols, and essentially compares terms lexicographically, recursively ensuring that no larger subterms are hidden deep in the term structure of the potentially smaller term.
As stated above, both LPO and KBO need to be instantiated with parameters - a symbol precedence in the case of LPO, both a symbol precedence and a weight assignment for KBO. In E, we have implemented 13 diferent mature precedence generation schemes, and 26 diferent mature weight assignment schemes. All are based on simple features of the signature (primarily arity) and the number of occurrences in the original input specification (frequency). E always generates the symbol precedence first, and the weight assignment scheme has the symbol precedence available as an extra input parameter.
Since any precedence can be combined with any weight assignment, this represents 13 diferent LPO instances, and 13 times 26, or 338 diferent KBO instances.
The complete list of precedence generation schemes used in the experiments is as follows: unary_first, unary_freq, arity, invarity, const_max, const_min, freq, invfreq, invconjfreq, invfreqconjmax, invfreqconjmin, invfreqconstmin, invfreqhack.
We will discuss some selected schemes in some detail - see [
As a simple and long-lived example, the arity function just orders symbols by
arity, making symbols with a bigger arity greater. Since all our schemes generate total
precedences, ties are broken by the order of appearance in the signature table (which
corresponds to the order in which symbols occur in the input). The unary_first scheme
is a variant that will make unary function symbols maximal. This allows the prover to
generate the ordering originally suggested in [
The 26 diferent weight assignment schemes are: firstmaximal0, arity, aritymax0, modarity, modaritymax0, aritysquared, aritysquaredmax0, invarity, invaritymax0, invaritysquared, invaritysquaredmax0, precedence, invprecedence, precrank5, precrank10, precrank20, freqcount, invfreqcount, freqrank, invfreqrank, invconjfreqrank, freqranksquare, invfreqranksquare, invmodfreqrank, invmodfreqrankmax0, constant.
An interesting case is firstmaximal0, which complements unary_first to generate the original KBO for group completion. It assigns a weight of 1 to all symbols, except to the first (non-constant) maximal symbol in the signature, which is assigned weight 0. A more complex example is invfreqconjmin. In this scheme, symbols are ordered by inverse frequency, but symbols that occur in the problem’s conjecture (if any) are smaller than symbols that occur only in axioms. Weights are then assigned sequentially, starting with 1 for the most frequent conjecture symbol. The precedence scheme assigns weights according to the (total) precedence, with symbols that are larger in the precedence also getting higher weights.
KBO also has the constraint that constants must have at least the weight of variables. In our experiments, we always assigned a fixed weight of 1 to both constants and variables.
One of the major advantages of superposition-based calculi is that they allow for strong redundancy elimination. One of the most important simplification techniques in practice is unconditional rewriting. It allows the use of a positive unit-equational clause (i.e. a single equation) to potentially replace a term in another clause by a smaller term. For this, two conditions have to be met2: On the one hand, one side of the equation (called the left-hand side or lhs) must match the subterm to be rewritten. And on the other hand, the instance used for rewriting must be decreasing, i.e. the instantiated other side (rhs) of the equation has to be strictly smaller than the replaced term. 2Rewriting is also restricted for a small set of term positions by the calculus, but that is not our concern here.
Most provers combine the matching and the instantiation operation. Thus, if an lhs matches a candidate term, the corresponding substitution is applied to both sides of the equation, and then the ordering condition is checked. This is often suficient, however, the test will automatically fail if the rhs contains a variable not occurring in the lhs, because such a free variable is always incomparable with any term in which it does not occur. To be able to still use these equations, we have introduced the concept of a strong instance of an equation. In a strong instance, we dynamically instantiate all variables of the equation before performing the ordering test. Variables in the lhs of an equation are automatically bound by the match against the term to be rewritten. Additionally, we substitute any remaining unbound rhs variables with the smallest constant (of the proper sort). As an example, consider the equation R = f (x, a) ' g(x, y) (where f is greater than g) applied to the term t = f (a, a) and let ⊥ be the smallest constant in the signature. The lhs f (x, a) matches t with σ = {x 7→ a}. But σ(R) = f (a, a) ' g(a, y) is unorientable. If we extend σ to also replace the unbound variable y by ⊥, we do get f (a, a) ' g(a, ⊥), which is orientable, and hence can be used to reduce the term. This is sound, because variables are universally quantified, i.e. the equality holds for all instances. We have implemented this simple concept in E, and it has shown a significant and consistent improvement in performance.
We have employed four diferent search strategies. All normal search parameters were
ifxed to (usually) known good values. The only diference between the four strategies was
in the clause selection heuristic. We broadly describe the 4 strategies below, see [
SC: This is a pure symbol-counting strategy. All function, predicate, and variable symbol occurrences are counted with a weight of one, and the lightest clauses are processed ifrst. The exact command line options for search control options are available in the online supporting material (see below). 20:1: This selection strategy interleaves selecting the lightest and the oldest clause, with a ratio of 20 to 1.
EVO: This clause selection strategy has been honed through various optimizations [
It interleaves a number of goal-directed and conventional selection queues, and is one of the best heuristics on TPTP we have found so far.
UEQ: This is similar to EVO in structure and intent, but optimised only towards unit-equational problems.
We ran tests on all suitable problems from TPTP 7.5.0. Most experiments were run on unit-equational problems. This set contained 1497 diferent problems. Some tests used all suitable first-order problems from TPTP (i.e. all CNF and FOF problems). This set was more than 10 times larger, containing 17283 problems. Run time per problem was limited to 5 seconds of CPU time.
Tests were run on a machine with four Intel Xeon Gold 6130 CPUs, running a total of 64 physical cores at a nominal frequency of 2.10GHz and with 512GB of RAM. RAM size was suficient to guarantee no contention or swapping between parallel processes.
We have run 351 diferent ordering schemes with 4 diferent search strategies and two diferent rewrite settings, i.e. 2808 diferent strategies, on 1497 UEQ problems, for a total of 4 203 576 individual UEQ test runs. We have run the same 351 strategies, with only the 20:1 clause selection strategy and conventional rewriting, on all 17283 problems for 6 066 333 individual test runs for the general case. Thus, the total corpus has data on a bit over 10 million test runs.
A version of the prover suitable for reproducing the actual dataset runs, as well as the summarized results of the test runs, is available as an online supplement at http: //eprover.eu/E-eu/Term_Orderings.html. The protocols included there also specify the exact command line options and contain the lists of problems used. TPTP 7.5.0, the source of the test problems, can be downloaded from http://www.tptp.org. The latest oficial release of E (and future updates) can be found at https://www.eprover.org.
We will first discuss the performance of the diferent orderings with conventional rewriting on the 1497 UEQ problems. Table 1 gives a general overview of the data. Each row corresponds to a search strategy (diferentiated by clause selection strategy and use of rewriting with strong instances). For each row, we show the number of problems solved by the best, worst, and median term ordering variant, and by the union of all variants, separately for LPO, KBO, and both.
We can see that the diference between the best and the worst ordering is roughly 110-120 successes, and about comparable to the diference between the weakest and strongest search strategy, which is roughly 130-145. We can also already see that for UEQ problems, the best LPO strategy is systematically worse than the worst KBO strategy. However, for each search strategy the union of both LPO and KBO strategies solves more problems than either alone.
To get a better understanding of the distribution of results, we have plotted the data in Fig. 2. In this figure, each individual measurement is a lightly coloured dot. The corresponding thin line is a gliding average. For each search strategy, the individual orderings are sorted in ascending order by number of successes. This results in a very distinct hockey stick graph, with an strongly ascending “blade”, followed by a more slowly rising “handle”. The blade consists of the results for the 13 diferent LPO instances, the handle of the 13 · 26 = 338 KBO instances. While this graph suggests very similar distribution of performance for each search strategies, it does not tell us if we see the same orderings in the same order, or if the diferent ordering variants appear in diferent order for the diferent search strategies.
To remedy this, we have replotted the same data in Fig. 3. In this figure, we use the SC strategy as the reference that determines the order of ordering variants for all 4 search
strategies. In other words, the ordering variants are represented by a fixed order on the X-axis for all diferent search strategies. We can see that the basic hockey stick shape remains, however, there is significant local variation, and the increase in the “handle” part of the graph is much less pronounced.
To quantify how far the order of strategies has changed between the diferent strategies,
we compute Kendall’s Tau value [
Performance on UEQ problems (by base performance)
Base (SC) 20:1 EVO
UEQ 0 null-hypothesis that the two rankings have been produced by uncorrelated processes.
All rankings are related to the SC base case. The correlation is quite weak for 20:1, but much stronger for the other strategies. The null-hypothesis can be comfortably rejected for all three pairings.
We can identify a number of consistently badly performing orderings. For all 4 search strategies, LPO with precedence generation schemata invarity and const_max are always among the worst 5 orderings. It’s less easy to pick out the winners, because the curves are fairly flat at the top. However, all strong orderings are KBO instances, and precedence schemata unary_first, const_min and invfreqconstmin appear frequently among the top strategies. For weight generation, invaritymax0 and invaritysquaredmax0 appear most frequently. The absolute best single combination is unary_first combined with firstmaximal0, however, there are 5 strategies with essentially the same performance.
Figure 4 shows the relative performance of the orderings for a CPU limit of 1 second, compared to a CPU limit of 5 seconds. For all 4 base strategies, there is good similarity between the curves, and for all but 20:1 there is a strong correlation. In all cases, the null-hypothesis is strongly rejected. Thus, it seems possible to extrapolate ordering performance from shorter to longer run times in most cases.
Performance for different CPU limits (SC)
Performance for different CPU limits (20:1) 50 100 150 200 250 300 350
Ordering strategies (by base strat successes) Performance for different CPU limits (Evo) 50 100 150 200 250 300 350 Ordering strategies (by base strat successes) Performance for different CPU limits (UEQ) Base (20:1 (1s)) 20:1 Base (UEQ (1s))
UEQ Base (SC (1s))
SC Base (EVO (1s)) EVO
We have plotted the relative performance of the diferent orderings and strategies in Figure 5. As already visible from the summary data in Table 1, rewriting with strong instances performs consistently better than conventional rewriting. The diference is significant for all base strategies but UEQ, where it is minuscule. In all 4 cases we have an excellent agreement between relative performance of normal and strong instance variants, indicating that strong instance can probably be added to any prover and yield an improvement without disrupting existing strategies.
Finally, we can compare the performance of all orderings on the full set of first-order problems, not just unit-equational problems. Since the number of problems is over 10 times larger now, we had to restrict the experiment to only one clause selection strategy. 720 700 680 s sse660 e c cuS640 620 600 580 880 860 840 sse820 s e ccu800 S 780 760 740 0 0 800 780 We picked 20:1, because it has decent performance and is easy to transfer to most other provers. The result is plotted in Figure 6. While the overall number of solutions for each ordering variant is several times higher for the full set (since the number of problems is higher), we can see that again performance on all problems correlates to performance on unit-equational problems, if not quite as pronounced as for some of the other comparisons.
The long term aim of this line of research is to automatically find good term orderings
for any given problem. Our current approach is driven by the very successful standard
saturation approach based on the given-clause loop. For the unit-equational case, there
has been a lot of impressive work done for the Waldmeister prover, some of which is
described in [
Relative performance on UEQ and all problems
Base (20:1) 20-1 Full 0 instantiated ordering schemes based on the domain. Generalising this approach to full clausal logic, and also automatising the knowledge acquisition, would be a major step into the future.
One step in this direction is the work by Bartek and Suda [
There has been some work about orienting a static system of equations with a KBO, e.g. [24]. However, this was a theoretical result with no experiments about the practical efects of computing such a static ordering before starting the proof search. Based on a similar premise is MaedMax [25], a completion-based system for unit-equality. It is not built on the given-clause loop, but rather on a kind of level-saturation. At each iteration of its main loop, the system tries to find an ordering to orient as many equations as possible before the next round, before computing and normalising all critical pairs of the resulting system.
Our work with strong instances is quite conservative, in that it does not modify the clause set or inference rules, but only makes the implementation correspond more closely to the theoretical case. Twee [26] has an interesting alternative approach. It splits such unorientable equations into an orientable part, and a permutation equation. It would be interesting to see a direct comparison of both techniques.
Finally, saturating theorem provers are moving into higher-order [27] . One significant question is how many of these techniques can be lifted to this case, and how well they will work there.
Term orderings are a critical component of the search strategies of modern theorem provers. We have presented a first systematic overview of the performance of relatively naive term ordering generation schemes. With respect to our research questions, we can say the following: 1. KBO performs almost uniformly better than LPO. However, both KBO and LPO instances are necessary to solve all solvable problems. Diferences between diferent LPO instances are much bigger than those between diferent KBO instances, but the latter are still significant. 2. There is some correlation between the performance of diferent orderings under diferent other settings. However, relative performance between similarly performing strategies cannot be reliably predicted. 3. It is, on the other hand, quite possible to predict relative performance for longer runtimes from shorter runtimes. That is particularly valuable for system tuning, since tuning experiments can be done with relatively short run times. 4. Maybe surprisingly, there is a quite good correlation between performance of an ordering in the UEQ domain and over all problems, despite the fact that orderings play additional roles for reasoning with general clauses.
The raw data is available for further evaluation and experiments, and there is a clear path to both generate more diverse and stronger orderings, and to couple ordering generation to the presence of certain axioms and axiom structures.
The various anonymous reviewers of this paper have been extremely helpful, identifying, in addition to several language issues and typos, a wrong number in Table 1 that slipped in during editing. pp. 525–542. [24] K. Korovin, A. Voronkov, Orienting rewrite rules with the Knuth–Bendix order,
Journal of Information and Computation 183 (2003) 165–186. [25] S. Winkler, G. Moser, MaedMax: A maximal ordered completion tool, in: D. Galmiche, S. Schulz, R. Sebastiani (Eds.), Proc. of the 9th IJCAR, Oxford, volume 10900 of LNAI, Springer, 2018, pp. 472–480. [26] N. Smallbone, Twee: An Equational Theorem Prover, in: A. Platzer, G. Sutclife (Eds.), Proc. of the 28th CADE, Pittsburgh, volume 12699 of LNAI, Springer, 2021, pp. 602–613. [27] P. Vukmirović, J. C. Blanchette, S. Cruanes, S. Schulz, Extending a Brainiac Prover to Lambda-free Higher-Order Logic, International Journal on Software Tools for Technology Transfer (2021). doi:10.1007/s10009-021-00639-7.