On Asymmetric Unification and the Combination Problem in Disjoint Theories

Serdar Erbatur 1 Deepak Kapur 2 Andrew Marshall 3 Catherine Meadows 3 Paliath Narendran 4 Christophe Ringeissen 5
5 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 : Asymmetric unification is a new paradigm for unification modulo theories that introduces irreducibility constraintson one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis, for which itis often necessary to put irreducibility constraints on portions of a state. However many facets of asymmetricunification thatare of particular interest, includingits behavior under combinations of disjoint theories, remain poorly understood.In this paper we give a new formulation of the method for unificationin the combination of disjoint equational theories developed by Baader and Schulz that bothgives additional insights into the disjoint combination problem in general, and furthermore allowsus to extend the method to asymmetric unification, giving the first unification method for asymmetric unification in the combination of disjoint theories.
Type de document :
Communication dans un congrès
Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Apr 2014, Grenoble, France. Springer, pp.15, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-642-54830-7_18〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01087065
Contributeur : Christophe Ringeissen <>
Soumis le : mardi 25 novembre 2014 - 14:34:40
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Serdar Erbatur, Deepak Kapur, Andrew Marshall, Catherine Meadows, Paliath Narendran, et al.. On Asymmetric Unification and the Combination Problem in Disjoint Theories. Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Apr 2014, Grenoble, France. Springer, pp.15, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-642-54830-7_18〉. 〈hal-01087065〉

Partager

Métriques

Consultations de la notice

238