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.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/inria-00527630
Contributor : Michaël Rusinowitch <>
Submitted on : Tuesday, October 19, 2010 - 6:06:57 PM
Last modification on : Thursday, October 17, 2019 - 8:56:44 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

442