Skip to Main content Skip to Navigation
Journal articles

Decidability of Equivalence of Symbolic Derivations

Yannick Chevalier 1, 2 Michael Rusinowitch 3
1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
IRIT - Institut de recherche en informatique de Toulouse
3 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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00527630
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Tuesday, October 19, 2010 - 6:06:57 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM

Links full text

Identifiers

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⟩

Share

Metrics

Record views

771