Term Ordering Diagrams

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 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.