AC Simplifications and Closure Redundancies in the Superposition Calculus

TL;DR

This paper extends AC joinability criteria from unit equalities to the superposition calculus and first-order logic, introducing new redundancy and demodulation criteria to improve theorem proving efficiency.

Contribution

It introduces a novel extension of AC joinability to superposition calculus and first-order logic, along with new redundancy and encompassment demodulation criteria.

Findings

Enhanced AC joinability criteria applicable to superposition calculus

New redundancy criterion covering ground joinability in AC contexts

Improved demodulation applicability across superposition theorem provers

Abstract

Reasoning in the presence of associativity and commutativity (AC) is well known to be challenging due to prolific nature of these axioms. Specialised treatment of AC axioms is mainly supported by provers for unit equality which are based on Knuth-Bendix completion. The main ingredient for dealing with AC in these provers are ground joinability criteria adapted for AC. In this paper we extend AC joinability from the context of unit equalities and Knuth-Bendix completion to the superposition calculus and full first-order logic. Our approach is based on an extension of the Bachmair-Ganzinger model construction and a new redundancy criterion which covers ground joinability. A by-product of our approach is a new criterion for applicability of demodulation which we call encompassment demodulation. This criterion is useful in any superposition theorem prover, independently of AC theories, and we demonstrate that it enables demodulation in many more cases, compared to the standard criterion.