Ground Associative and Commutative Completion Modulo Shostak Theories

Sylvain Conchon 1, 2 Evelyne Contejean 1, 2 Mohamed Iguernelala 1, 2
2 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. In the ground case, 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. The main ideas of our algorithm are first to adapt the definition of rewriting in order to integrate the canonizer of X and second, to replace the equation orientation mechanism found in ground AC-completion with the solver for X
Type de document :
Communication dans un congrès
LPAR, Oct 2010, Yogyakarta, Indonesia. 2010
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00535652
Contributeur : Sylvain Conchon <>
Soumis le : vendredi 12 novembre 2010 - 11:32:05
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:30:34

Fichier

conchon-lpar17-short.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00535652, version 1

Collections

Citation

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. LPAR, Oct 2010, Yogyakarta, Indonesia. 2010. 〈inria-00535652〉

Partager

Métriques

Consultations de la notice

170

Téléchargements de fichiers

95