Term Ordering Diagrams

TL;DR

This work tackles the heavy cost of term-ordering checks in saturation-based theorem proving by introducing term ordering diagrams ($\text{TOD}$), a lazy-indexing structure that speeds up post-ordering checks under substitutions for orders such as the Knuth–Bendix order ($KBO$) and the lexicographic path order ($LPO$). TODs support on-demand transformations that preserve equivalence and enable reuse of computation history to accelerate equality retrieval and forward demodulation. The authors prove termination and equivalence of TOD transformations, describe a retrieval algorithm parameterized by a forcing function, and implement TODs in Vampire, showing substantial improvements on $\text{TPTP}$ UEQ problems and broader speedups for $LPO$ and $KBO$ configurations. The practical impact is a significant reduction in post-ordering cost, enabling faster automated reasoning with potential extensions to other orders and related deduction tasks, albeit with memory tradeoffs due to stored ordering data.

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.