Decidability of Equivalence of Symbolic Derivations

Yannick Chevalier 1 Michael Rusinowitch 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We give in this paper an alternative, and we believe simpler, proof of a deep result by Mathieu Baudet, namely that the equivalence of symbolic constraints is decidable for deduction systems on a finite signature modulo a subterm convergent equational theory.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.263-292. 〈10.1007/s10817-010-9199-5〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00527630
Contributeur : Michaël Rusinowitch <>
Soumis le : mardi 19 octobre 2010 - 18:06:57
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Yannick Chevalier, Michael Rusinowitch. Decidability of Equivalence of Symbolic Derivations. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.263-292. 〈10.1007/s10817-010-9199-5〉. 〈inria-00527630〉

Partager

Métriques

Consultations de la notice

375