episciences.org_1034_1628060977
1628060977
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
1860-5974
09
14
2012
Volume 8, Issue 3
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories :
Design and Implementation
Sylvain
Conchon
Evelyne
Contejean
Mohamed
Iguernelala
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.
Comment: 30 pages, full version of the paper TACAS'11 paper "Canonized
Rewriting and Ground AC-Completion Modulo Shostak Theories" accepted for
publication by LMCS (Logical Methods in Computer Science)
09
14
2012
1034
arXiv:1207.3262
10.2168/LMCS-8(3:16)2012
https://lmcs.episciences.org/1034