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

Sylvain Conchon 1, 2 Evelyne Contejean 2 Mohamed Iguernelala 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (3:16), pp.1-29. 〈http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40〉. 〈10.2168/LMCS-8(3:16)2012〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00798082
Contributeur : Evelyne Contejean <>
Soumis le : vendredi 8 mars 2013 - 07:13:28
Dernière modification le : jeudi 5 avril 2018 - 12:30:09

Lien texte intégral

Identifiants

Collections

Citation

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (3:16), pp.1-29. 〈http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40〉. 〈10.2168/LMCS-8(3:16)2012〉. 〈hal-00798082〉

Partager

Métriques

Consultations de la notice

185