Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

TL;DR

This paper introduces AC(X), a modular extension of ground AC-completion that combines associative-commutative reasoning with Shostak theories, enabling decision procedures for complex formulas in theorem proving.

Contribution

It presents a novel, modular algorithm that integrates canonized rewriting with Shostak theories into AC-completion, extending its applicability and efficiency.

Findings

Proved AC(X) is sound, complete, and terminating.

Implemented AC(X) in the Alt-Ergo theorem prover.

Demonstrated effectiveness in deciding formulas involving AC symbols and Shostak theories.

Abstract

AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X. Our algorithm, called AC(X), is obtained by augmenting in a modular way ground AC-completion with the canonizer and solver present for the theory X. This integration rests on canonized rewriting, a new relation reminiscent to normalized rewriting, which integrates canonizers in rewriting steps. AC(X) is proved sound, complete and terminating, and is implemented to extend the core of the Alt-Ergo theorem prover.