Conchon, Sylvain and Contejean, Evelyne and Iguernelala, Mohamed - Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

lmcs:1034 - Logical Methods in Computer Science, September 14, 2012, Volume 8, Issue 3
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

Authors: Conchon, Sylvain and Contejean, Evelyne and Iguernelala, Mohamed

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.


Source : oai:arXiv.org:1207.3262
DOI : 10.2168/LMCS-8(3:16)2012
Volume: Volume 8, Issue 3
Published on: September 14, 2012
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science,F.4.1, G.4


Share

Browsing statistics

This page has been seen 18 times.
This article's PDF has been downloaded 3 times.