Skip to Main content Skip to Navigation
New interface
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
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Tuesday, October 19, 2010 - 6:06:57 PM
Last modification on : Monday, July 4, 2022 - 9:04:30 AM

Links full text



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



Record views