Ground Associative and Commutative Completion Modulo Shostak Theories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Ground Associative and Commutative Completion Modulo Shostak Theories

Résumé

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
Fichier principal
Vignette du fichier
conchon-lpar17-short.pdf (81.66 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00535652 , version 1 (12-11-2010)

Identifiants

  • HAL Id : inria-00535652 , version 1

Citer

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala. Ground Associative and Commutative Completion Modulo Shostak Theories. LPAR, Oct 2010, Yogyakarta, Indonesia. ⟨inria-00535652⟩
78 Consultations
136 Téléchargements

Partager

Gmail Facebook X LinkedIn More