Pith. sign in

REVIEW 1 major objections 5 minor 45 references

Term Ordering Diagrams

T0 review · 1 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Term ordering diagrams index repeated post-ordering checks so that equational provers reuse, rather than recompute, KBO and LPO comparisons.

desk verdict A solid, useful contribution on post-ordering checks in saturation provers; a real specification gap on positivity-check semantics needs closing. read the letter →

arxiv 2505.22181 v1 pith:KF5HXYNA submitted 2025-05-28 cs.LO

Márton Hajdu , Robin Coutelier , Laura Kovács , Andrei Voronkov This is my paper
classification cs.LO MSC 68T1503B35
keywords termorderingdiagramspost-orderingproblemindexingKnuth-Bendixorderlexicographicpathsuperpositioncalculusdemodulationautomatedtheoremproving
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces term ordering diagrams (TODs), a lazy index for the post-ordering checks that saturation provers make when they repeatedly ask whether a substitution turns an unordered equality into a usable demodulator or superposition premise. A TOD stores the structure of KBO and LPO comparisons as a directed acyclic graph of term-comparison and weight-sign nodes, and every traversal rewrites the diagram locally so that later queries reuse facts already learned. The paper proves that these rewrites preserve the success set for every query substitution, and reports that in unit-equality problems the share of instructions spent on post-ordering checks falls from roughly $52\%$ to between $18\%$ and $24\%$ when TODs are shared per left-hand side. If this is right, ordering checks stop being one of the dominant costs of equational reasoning, and the saved time can go into the proof search itself.

What carries the argument

The central object is the term ordering diagram (TOD), a directed acyclic graph with a single root and a single exit. Each evaluation node carries either a term comparison $s>?t$ with outgoing edges labelled $>$, $=$, and $\ngeq$, or a KBO positivity check $e\geq?0$ with edges labelled $>$, $\geq$, and $\ngeq$; success nodes are labelled by equalities. The load-bearing mechanism is the set of node-local rewrite rules derived from the recursive clauses of KBO and LPO, together with a forcing rule: a node forces an edge label when every substitution that reaches the node must take that edge, and such nodes can be removed. Node replication guarantees that a visited node has a single incoming path, which is what makes the forcing analysis local and lets the paper state correctness as equivalence of success sets over all substitutions.

What would settle it

Run the retrieval algorithm on a small unit-equality problem whose weight difference is non-ground, such as $y-x$, and compare its answer with a brute-force post-ordering check that enumerates all grounding substitutions on a finite signature; any substitution for which the two answers differ falsifies the correctness claim.

Watch

Extended reading notes

Core claim

A post-ordering check does not have to be re-derived from scratch each time it is asked. The paper's claim is that the whole family of checks for one left-hand side can be organised as a term ordering diagram: a rooted DAG whose evaluation nodes are term comparisons $s>?t$ and, for KBO, weight-sign checks $e\geq?0$, and whose success nodes hold the equalities that may be retrieved. Traversing the diagram for a query substitution $\sigma$, following the edge selected by evaluating each node under $\sigma$, returns exactly the equalities with $l\sigma\succ r_i\sigma$. The retrieval algorithm rewrites the diagram on the fly: nodes that force an edge label are removed, nodes with several incoming paths are replicated, and a comparison of $f(\bar s)>?g(\bar t)$ is expanded according to the KBO or LPO clauses. The paper proves each rewrite preserves the success set for every substitution, and its experiments show that doing these rewrites lazily, only on nodes actually visited, makes checks cheaper over time, with the larger gains on LPO.

Load-bearing premise

The load-bearing premise is that the prover's sign test for a non-ground linear expression $e$ means exactly the paper's universal semantics: $e>0$ when $\sigma(e)>0$ for every grounding substitution, and $e\geq0$ when $\sigma(e)\geq0$ for every grounding substitution; if the implemented test uses a different convention, a transformed TOD could follow a branch that the correctness proof does not justify.

Editorial extensions

If this is right

  • Lazy rewriting turns repeated post-ordering checks on the same left-hand side from full KBO or LPO re-evaluations into short traversals, so the cost of a check is amortised over many demodulation attempts.
  • In the unit-equality regime with LPO, the post-ordering share of instructions drops from roughly $52\%$ to about $18\%$ with shared TODs, and more benchmark problems are solved within the same time limit.
  • Because the transformations preserve the success set, equalities can be inserted into the index freely, and deletion is handled by marking clauses as deleted instead of restructuring the diagram.
  • Sharing one TOD across all equalities with the same left-hand side is stronger than a per-equality TOD, because information learned while checking one equality immediately rules out or confirms others.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same node-local rewrite idea should transfer to other simplification orders whose definitions are a small set of recursive clauses; only the KBO/LPO-specific expansion rules would need to be replaced, for example for a weighted path order.
  • Because the index is queried by substitution and rewritten lazily, TOD-style caching could also apply to other substitution-dependent side conditions in saturation, such as constrained superposition or ground-reducibility checks.
  • The memory increase observed in some runs suggests a testable extension: a policy that bounds TOD size or forgets rarely visited branches could trade a little speed for much lower memory, a tradeoff the paper leaves implicit.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper introduces term ordering diagrams (TODs), a DAG-based index for the post-ordering problem: given equalities l≈r1,...,l≈rn with a common left-hand side and a substitution σ, retrieve those with lσ≻riσ. TODs interleave term comparison nodes and, for KBO, positivity check nodes, and are modified lazily during traversal by equivalence-preserving transformations derived from the KBO/LPO definitions (Figures 4–5) plus generic node removal and replication (Figure 3). The authors prove termination and equivalence of the transformations (Theorem 1), give a retrieval algorithm with termination and correctness lemmas (Lemmas 1–4), implement the approach in Vampire, and report reduced instruction counts for post-ordering checks and forward demodulation, with the strongest gains in LPO/UEQ problems.

Significance. If correct, the TOD construction addresses a real bottleneck in saturation-based equational reasoning: the repeated checks of whether an unordered equality becomes orderable after substitution. The formal development is a genuine contribution: the transformations are derived from the KBO/LPO definitions rather than fitted to experimental data, the correctness proof for the transformations is a detailed case analysis (Appendix A), and the retrieval algorithm is accompanied by termination and equivalence lemmas. The experimental evaluation is thorough for the area, reporting problem counts, calibrated instruction counts, memory behavior, and per-problem distributions; the shared-TOD variant reduces the post-ordering instruction share in UEQ/LPO runs from about 52% to 18–24% (Table 3). The main caveat is that the soundness of the implemented variant rests on an unstated decision procedure for positivity checks on non-ground linear expressions.

major comments (1)
  1. [Section 2–3, Figure 4/10, Appendix A] The KBO branch condition e≥?0 is defined semantically: σ(e≥?0) is >, ≥, or ≱ according to whether the linear expression σ(e) is >0, ≳0, or neither, where >0 and ≳0 are universal over grounding substitutions. The KBO transformations branch on this check, and the proof of Theorem 1 (Appendix A, cases (1)–(5)) assumes the traversal follows the edge selected by this universal semantics. However, the manuscript never specifies how Vampire decides whether a non-ground linear expression such as 2x−y−1 is universally positive or non-negative over grounding substitutions, nor does it cite an external decision procedure for this subproblem. A syntactic sign test on the concrete substituted expression is not equivalent to the universal semantics, because the set of weights of ground terms is constrained by w0>0 and by the signature; for example, an expression with a negative variable coefficient can be non-negative on all ground terms, while a syntactically positive expression can fail to be universally positive. Remark 1 explicitly leaves positivity-check-derived term constraints out of the forcing function, so the forcing function cannot repair this gap. Please specify the implemented sign test (or the KBO constraint-solving algorithm from [8,9,19] used) and prove that it matches the Section 2 semantics; without this, Theorem 1 and Lemma 4 do not establish soundness of the implemented TOD retrieval.
minor comments (5)
  1. [Section 5, Figure 6] The insertion operation is described as inserting a node “just before the exit node,” but a general TOD can have many edges into the exit node; please state whether the new comparison node is spliced into every such edge or attached as a new shared predecessor, and how the single-incoming-edge invariant used in Lemma 1 is maintained.
  2. [Section 2–3] The symbol σ is used both for an arbitrary grounding substitution in the definitions of e>0 and e≳0 and for the query substitution in the definitions of Section 3; this double use makes the semantics of σ(e≥?0) harder to follow and should be renamed in one of the two places.
  3. [Definition 2 vs. Section 5, step 1] Definition 2 defines the success set as the labels of all success nodes on the traversal path, while the retrieval algorithm returns only non-deleted equalities; the definition of TOD equivalence should be stated with deletions in mind or the definition should be adjusted accordingly.
  4. [Figure 7, step 2 and Example 3] The example says a success node is “marked visited (step 3c)”, but step 3 in Figure 7 applies only to unvisited evaluation nodes; either mark success nodes visited explicitly in step 2 or omit this from the example.
  5. [Appendix D.2] The phrase “multiplied … by an order of 100” is imprecise; the described example increases the non-demodulation share by a factor of about 106, not 100.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: TOD transformations are derived from KBO/LPO definitions and the speedups are externally measured; the positivity-check implementation gap is a soundness concern, not a circular derivation.

full rationale

The paper's derivation chain is self-contained. Theorem 1 is proved in Appendix A by case analysis directly from the KBO clauses (K1)-(K3) and LPO clauses (L1)-(L3): for instance, when sigma(|s|-|t|)>0, (K1) yields the original '>' edge and the replacement positivity node also leads to n1, and the remaining cases check the '>=' and 'not>=' paths. This is a soundness proof relative to the definitions of Sections 2-3, not a reuse of the target claim. The generic redundant-node-removal transformation is justified by Definition 2's 'forces' predicate: if every traversal reaching a node takes label l, bypassing the node cannot change the success set, so TOD equivalence follows semantically. The forcing function in Definition 4 has exactly the property used in Lemma 2, so it does not smuggle in the conclusion. The experimental claims (Tables 1-3) are direct measurements of externally supplied TPTP problems and instruction counters, with no parameter fitted to the reported post-ordering reductions. The only manuscript-internal concern is the unspecified computation of positivity checks for non-ground linear expressions: Section 2 defines e>0 universally over grounding substitutions, while Section 3's traversal semantics applies sigma(e>=?0) to a concrete query, so the paper does not state how Vampire decides the sign symbolically. This is a soundness/implementation gap, and Remark 1's limitation about term-constraint reasoning confirms the forcing function is an approximation, but neither makes any prediction equivalent to its input by construction. Self-citations [20,21] are contextual: they motivate runtime specialization, but the TOD correctness proof does not depend on them.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters or invented physical entities. The work relies on standard properties of KBO/LPO and on the modeling assumption that indexed equalities share a left-hand side.

assumptions (4)
  • standard math KBO is a simplification ordering whenever w0>0 and every unary function symbol of weight 0 is minimal in the precedence.
    Stated in Section 2 as a known condition; used by the KBO transformations in Figures 4 and 10.
  • standard math LPO is a simplification ordering for any precedence.
    Stated in Section 2; used by the LPO transformations in Figures 5 and 11.
  • domain assumption The transitivity axioms (tr1)-(tr5) are valid for term constraints built from a simplification ordering and syntactic equality.
    Introduced in Appendix B to compute the transitive closure used by the forcing function; they follow from the ordering being a strict partial order with equality, but are not proven in the paper.
  • domain assumption The post-ordering problem is restricted to equalities with a common left-hand side l.
    Definition in Section 1; justified by the use of a separate term index to retrieve l in demodulation, but it is an assumption that limits the scope.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Term Ordering Diagrams." pith.science (2026). https://pith.science/paper/KF5HXYNA

@misc{pith2026250522181,
  author       = {Pith},
  title        = {Pith review of: Term Ordering Diagrams},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KF5HXYNA}},
  note         = {Machine review of arXiv:2505.22181}
}
read the original abstract

The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) for discovering redundant clauses and inferences. Implementing term orderings is however challenging. While KBO comparisons can be performed in linear time and LPO checks in quadratic time, using the best known algorithms for these orders is not enough. Indeed, our experiments show that for some examples term ordering checks may use about 98% of the overall proving time. The reason for this is that some equalities that cannot be ordered can become ordered after applying a substitution (post-ordered), and we have to check for post-ordering repeatedly for the same equalities. In this paper, we show how to improve post-ordering checks by introducing a new data structure called term ordering diagrams, in short TODs, which creates an index for these checks. We achieve efficiency by lazy modifications of the index and by storing and reusing information from previously performed checks to speed up subsequent checks. Our experiments demonstrate efficiency of TODs.

Figures

Figures reproduced from arXiv: 2505.22181 by the authors.

Figure 1
Figure 1. Equality retrievals, where l def = f(x, y), r1 def = f(y, x) and r2 def = f(x, x). (a) and (b) show retrieval of l ≈ r1, where (a) contains a term comparison l >? r1 and (b) is a simplified version of (a) with term comparison x >? y. Further, (c) and (d) show retrieval of l ≈ r2, where (c) contains term comparison l >? r2 and (d) is a simplified version of (c) with a positivity check y − x ≥ ? 0 and term comparison … view at source ↗
Figure 2
Figure 2. Retrieving multiple equalities, where l def = f(x, y), r1 def = f(y, x) and r2 def = f(x, x). The success set of the T traversal for σ is the set of labels of all success nodes on this path; we also refer to it as the success set of σ in T . For any non-exit node in a traversal, we refer to its next edge and next node. For a node n labeled by c, where c is either a term comparison or a positivity check, we say that … view at source ↗
Figure 3
Figure 3. Generic transformations on TODs: (a) redundant node removal, where node n forces label ℓ; and (b) node replication, where n2 is an exact copy of a non-exit node n that has multiple incoming edges. Definition 3 (TOD Equivalence). Two TODs T1 and T2 are equivalent if for every substitution σ, the success sets of σ in T1 and T2 coincide. ❏ 4 TOD Transformations We explain our TOD transformations via a sequence of subgr… view at source ↗
Figures from the paper (12 more)
Figure 4
Figure 4. Figure 4: KBO transformations on TODs. Proof. (1) For proving termination, we introduce a well-founded order on TODs and show that every transformation replaces a TOD by a smaller one. In the proof, we use (well-founded) finite multiset extensions of (well-founded) orders. We fi…
Figure 5
Figure 5. Figure 5: LPO transformations on TODs. comparison node f(¯s) >? f(t¯) by a finite number of paths, so that every new term comparison node on these paths contains a comparison of a pair of terms strictly smaller in the multiset order than the multiset {f(¯s), f(t¯)}. Another exam…
Figure 6
Figure 6. Figure 6: Insertion of l ≈ r Index operations. The insertion of an equality l ≈ r is simple: we insert a term comparison node just before the exit node, as shown in [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]
Figure 7
Figure 7. Figure 7: Retrieval algorithm steps. Lemma 2. Step 3a of [PITH_FULL_IMAGE:figures/full_fig_p012_7.png]
Figure 8
Figure 8. Figure 8: Retrieval with a query substitution σ such that xσ = yσ. 1. Starting with sub-diagram A of [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]
Figure 9
Figure 9. Figure 9: Result of insertion of f(x, y) ≈ f(x, x) into the TOD of in sub-diagram F of [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: KBO transformations on TODs (repeated). of the “forces” relation (Definition 2). Node replication preserves equivalence because the set of paths in the TOD does not change. Let n be a term comparison node labeled with s >? t in T and let s = f(s1, . . . , sk) and t = …
Figure 11
Figure 11. Figure 11: LPO transformations on TODs (repeated). (2) g ≫ f. In the k = 0 case, the T traversal for σ contains n3, and we replace n by n3 in T ′ , so the T ′ traversal for σ contains n3 too. Otherwise k > 0. In this case, we also add k − 1 new nodes to T ′ . Let us denote n in …
Figure 12
Figure 12. Figure 12: Vampire run times with -to kbo. We show -sa discount in the left column and -sa otter in the right column. In each column, we compare -fdtod values off with on (top), off with shared (middle), and on with shared (bottom) [PITH_FULL_IMAGE:figures/full_fig_p035_12.png]
Figure 13
Figure 13. Figure 13: Vampire run times with -to lpo. We show -sa discount in the left column and -sa otter in the right column. In each column, we compare -fdtod values off with on (top), off with shared (middle), and on with shared (bottom) [PITH_FULL_IMAGE:figures/full_fig_p036_13.png]
Figure 14
Figure 14. Figure 14: Proportion of number of instructions spent in forward demodulation over the overall number of instructions. We show -to kbo in the left column, -to lpo in the right column; -sa discount in the top row, and -sa otter in the bottom row. All runs were limited to 200 × 10…
Figure 15
Figure 15. Figure 15: Proportion of number of instructions spent in post-ordering checks over the overall number of instructions. We show -to kbo in the left column, -to lpo in the right column; -sa discount in the top row, and -sa otter in the bottom row. All runs were limited to 200 × 10…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

45 extracted references · 30 canonical work pages

  1. [1]

    ACM TOCL (2003)

    Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch, M.: Deciding the confluence of ordered term rewrite systems. ACM TOCL (2003). https://doi.org/10.1145/601775.601777

    arXiv 2003

  2. [2]

    Journal of Automated Reasoning (1997)

    Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - A Distributed and Learning Equational Prover. Journal of Automated Reasoning (1997). https://doi.org/10.1023/A:1005879229581

    work page doi:10.1023/a:1005879229581 1997

  3. [3]

    In: IJCAR (2022)

    Duarte, A., Korovin, K.: Ground Joinability and Connectedness in the Superposi- tion Calculus. In: IJCAR (2022). https://doi.org/10.1007/978-3-031-10769-6 11

    doi:10.1007/978-3-031-10769-6 2022

  4. [4]

    In: IJCAR (2020)

    Gleiss, B., Kov´ acs, L., Rath, J.: Subsumption Demodulation in First-Order Theo- rem Proving. In: IJCAR (2020). https://doi.org/10.1007/978-3-030-51074-9 17

    doi:10.1007/978-3-030-51074-9 2020

  5. [5]

    Unpub- lished manuscript (1980)

    Kamin, S., L´ evy, J.J.: Two generalizations of the recursive path ordering. Unpub- lished manuscript (1980)

    work page 1980

  6. [6]

    In: Automation of Reasoning 2

    Knuth, D.E., Bendix, P.B.: Simple Word Problems in Universal Algebras. In: Automation of Reasoning 2. Springer (1983). https://doi.org/10.1007/978-3-642- 81955-1 23

    doi:10.1007/978-3-642- 1983

  7. [7]

    In: IJCAR (2008)

    Korovin, K.: iProver — An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: IJCAR (2008). https://doi.org/10.1007/978-3-540- 71070-7 24

    doi:10.1007/978-3-540- 2008

  8. [8]

    In: ICALP (2001)

    Korovin, K., Voronkov, A.: Knuth-Bendix Constraint Solving Is NP-Complete. In: ICALP (2001). https://doi.org/10.1007/3-540-48224-5 79

    doi:10.1007/3-540-48224-5 2001

Show all 45 references
  1. [9]

    Information and Computation (2003)

    Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth–Bendix order. Information and Computation (2003). https://doi.org/10.1016/S0890- 5401(03)00021-X

    2003 doi

  2. [10]

    Kov´ acs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV. pp. 1–35 (2013). https://doi.org/10.1007/978-3-642-39799-8 1

    2013 doi

  3. [12]

    International Journal on Artificial Intelligence Tools (2006)

    L¨ ochner, B.: Things To Know When Implementing LPO. International Journal on Artificial Intelligence Tools (2006). https://doi.org/10.1142/S0218213006002564

    2006 doi

  4. [13]

    In: IWIL (2001), https://www.researchgate.net/publication/229079124

    L¨ ochner, B., Schulz, S.: An Evaluation of Shared Rewriting. In: IWIL (2001), https://www.researchgate.net/publication/229079124

    2001

  5. [14]

    Journal of Automated Reasoning (2006)

    L¨ ochner, B.: Things to Know when Implementing KBO. Journal of Automated Reasoning (2006). https://doi.org/10.1007/s10817-006-9031-4

    2006 doi

  6. [15]

    Journal of Automated Reasoning (1997)

    McCune, W., Wos, L.: Otter - the CADE-13 competition incarnations. Journal of Automated Reasoning (1997). https://doi.org/10.1023/A:1005843632307

    1997 doi

  7. [16]

    In: Hand- book of Automated Reasoning, chap

    Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Hand- book of Automated Reasoning, chap. 7. Elsevier and MIT Press (2001). https://doi.org/10.1016/B978-044450813-3/50009-6

    2001 doi

  8. [17]

    Information Processing Letters (1993)

    Nieuwenhuis, R.: Simple LPO constraint solving methods. Information Processing Letters (1993). https://doi.org/10.1016/0020-0190(93)90226-Y 18 M´ arton Hajdu, Robin Coutelier, Laura Kov´ acs and Andrei Voronkov

    1993 doi

  9. [18]

    In: CADE (1999)

    Nieuwenhuis, R.: Invited Talk: Rewrite-Based Deduction and Symbolic Con- straints. In: CADE (1999). https://doi.org/10.1007/3-540-48660-7 28

    1999 doi

  10. [19]

    Information and Computation (2002)

    Nieuwenhuis, R., Rivero, J.M.: Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Information and Computation (2002). https://doi.org/10.1006/inco.2002.3146

    2002

  11. [20]

    In: JELIA (2000)

    Riazanov, A., Voronkov, A.: Partially Adaptive Code Trees. In: JELIA (2000). https://doi.org/10.1007/3-540-40006-0 15

    2000 doi

  12. [21]

    In: CADE (2004)

    Riazanov, A., Voronkov, A.: Efficient Checking of Term Ordering Constraints. In: CADE (2004). https://doi.org/10.1007/978-3-540-25984-8 3

    2004 doi

  13. [22]

    In: CADE (2019)

    Schulz, S., Cruanes, S., Vukmirovi´ c, P.: Faster, Higher, Stronger: E 2.3. In: CADE (2019). https://doi.org/10.1007/978-3-030-29436-6 29

    2019 doi

  14. [23]

    In: Handbook of Au- tomated Reasoning, chap

    Sekar, R., Ramakrishnan, I., Voronkov, A.: Term Indexing. In: Handbook of Au- tomated Reasoning, chap. 26. MIT Press (2001). https://doi.org/10.1016/B978- 044450813-3/50028-X

    2001 doi

  15. [24]

    AI Magazine (2016)

    Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Magazine (2016). https://doi.org/10.1609/aimag.v37i2.2620

    2016 doi

  16. [25]

    In: IJCAR (2024)

    Sutcliffe, G.: Stepping Stones in the TPTP World. In: IJCAR (2024). https://doi.org/10.1007/978-3-031-63498-7 3

    2024 doi

  17. [26]

    Journal of Automated Reasoning (2022)

    Vukmirovic, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making Higher-Order Superposition Work. Journal of Automated Reasoning (2022). https://doi.org/10.1007/s10817-021-09613-z

    2022 doi

  18. [27]

    Science of Computer Programming (2015)

    Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Science of Computer Programming (2015). https://doi.org/10.1016/j.scico.2014.07.009 Appendix A Correctness of TOD Transformations In this section, we present a detailed proof of our main result. ...

    2015 doi

  19. [28]

    x ⩾̸y due to x<f (x) and f(x) ⩾̸y, using axiom (tr5),

  20. [29]

    z >y due to y <g(y) and g(y) =z, using axiom (tr3),

  21. [30]

    Since x ⩾̸ z is implied by TR∧ F , we conclude that the node labeled x >? z forces label ≱

    x ⩾̸z due to x ⩾̸y and y <z, using axiom (tr4). Since x ⩾̸ z is implied by TR∧ F , we conclude that the node labeled x >? z forces label ≱. ❏ 26 M´ arton Hajdu, Robin Coutelier, Laura Kov´ acs and Andrei Voronkov Remark 1. It is possible to further strengthen reasoning over te...

  22. [31]

    apply σ on s and θ on t, resulting in the terms s′ and t′, respectively,

  23. [32]

    We noted earlier that KBO and LPO can be implemented in linear, respectively quadratic time in the size of the compared terms [14,12]

    compare s′ and t′ using≻, that is, determine whether s′≻ t′, s′ = t′ or s′≺t′ holds. We noted earlier that KBO and LPO can be implemented in linear, respectively quadratic time in the size of the compared terms [14,12]. However, we can still improve the above steps using the f...

  24. [33]

    traversing all non-variable subterms of s as if they were subterms of s′,

  25. [34]

    For this, we have to work on pairs of terms and substitutions, as defined below

    applying the substitution only when reaching a variable x ins, in which case we continue traversal in xσ. For this, we have to work on pairs of terms and substitutions, as defined below. Definition 7 (Closure Term). Lets be a term and σ a substitution. We call the pair s·σ a c...

  26. [35]

    We get a·ε =a·θ, which is true by case (1) since a is ground

    For x·σ =a·θ, case (2) applies. We get a·ε =a·θ, which is true by case (1) since a is ground

  27. [36]

    We get b·σ =b·ε, which is true by case (1) since b is ground

    For b·σ =y·θ, case (3) applies. We get b·σ =b·ε, which is true by case (1) since b is ground. ❏ For KBO, we define linear expressions for closure terms as follows. 7 This is usually a pointer comparison taking constant time. Term Ordering Diagrams 29 Definition 9 (Linear Expre...

  28. [37]

    Finally,f(z,u )·ε≻lpo z·ε holds due to (L1) and f(z,u )≻lpo z

    check x·σ≻lpo x·θ: (L2) applies, so we compare f(z,u )·ε and x·θ, then (L3) applies, so we compare f(z,u )·ε and z·ε. Finally,f(z,u )·ε≻lpo z·ε holds due to (L1) and f(z,u )≻lpo z. 30 M´ arton Hajdu, Robin Coutelier, Laura Kov´ acs and Andrei Voronkov

  29. [38]

    This holds by (L1) and f(z,u )≻lpo u

    check f(x,y )·σ≻lpo y·θ: (L3) applies, so we comparef(x,y )·σ≻lpo f(u,z )·ε, then (L4) applies, so we perform the following subcomparisons: (a) check x·σ≻lpo u·ε, which by (L2) is equivalent to checkingf(z,u )·ε≻lpo u·ε. This holds by (L1) and f(z,u )≻lpo u. (b) check f(x,y )·...

  30. [39]

    We compute the linear expression |s|−| t|

  31. [40]

    If either (K1) or (K2) applies, we exit early with success

  32. [41]

    If none of (K1)–(K3) applies, we exit early with failure

  33. [42]

    for free

    Otherwise, we check if (K3) applies recursively. This algorithm clearly takes quadratic time in the sizes of s and t. However, instead of always computing the linear expressions from scratch, we utilize term sharing to memoize the linear expressions for terms that we have alre...

  34. [43]

    baseline uses bidirectional comparison without closure terms,

  35. [44]

    conf1 uses bidirectional comparison with closure terms,

  36. [45]

    conf2 uses unidirectional comparison without closure terms,

  37. [46]

    queries” represent the number of retrievals for TODs, whereas “answers

    conf3 uses unidirectional comparison with closure terms. Our experiments were run with a 60-second timeout. The results are shown in Tables 4 and 5. The tables show that both unidirectional comparisons and comparisons with closure terms improve the running times and also the n...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.