Skip to Main content Skip to Navigation
Journal articles

Decidability of Equivalence of Symbolic Derivations

Yannick Chevalier 1 Michael Rusinowitch 2
1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
IRIT - Institut de recherche en informatique de Toulouse
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.
Document type :
Journal articles
Complete list of metadatas
Contributor : Michaël Rusinowitch <>
Submitted on : Tuesday, October 19, 2010 - 6:06:57 PM
Last modification on : Tuesday, October 27, 2020 - 2:34:28 PM

Links full text



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⟩



Record views