Term Ordering Diagrams
M\'arton Hajdu, Robin Coutelier, Laura Kov\'acs, Andrei Voronkov

TL;DR
This paper introduces term ordering diagrams (TODs), a new data structure that significantly improves the efficiency of term ordering checks in theorem proving, especially for repeated post-ordering scenarios.
Contribution
The paper presents TODs, a novel data structure that optimizes term ordering checks by enabling lazy updates and reuse of previous results, enhancing theorem prover performance.
Findings
TODs reduce term ordering check times substantially.
Experiments show TODs improve overall proving efficiency.
Post-ordering checks become more scalable with TODs.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNatural Language Processing Techniques · Formal Methods in Verification · Logic, Reasoning, and Knowledge
