Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 constraints on one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis, for which it is often necessary to put irreducibility constraints on portions of a state. However many facets of asymmetric unification that are of particular interest, including its behavior under combinations of disjoint theories, remain poorly understood. In this paper we give a new formulation of the method for unification in the combination of disjoint equational theories developed by Baader and Schulz that both gives additional insights into the disjoint combination problem in general, and furthermore allows us to extend the method to asymmetric unification, thus giving the first unification method for asymmetric unification in the combination of disjoint theories.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Friday, February 14, 2014 - 4:17:10 PM
Last modification on : Friday, November 18, 2022 - 9:25:01 AM
Long-term archiving on: : Thursday, May 15, 2014 - 10:43:03 AM


Files produced by the author(s)


  • HAL Id : hal-00947088, version 1


Serdar Erbatur, Deepak Kapur, Andrew Marshall, Catherine Meadows, Paliath Narendran, et al.. Asymmetric Unification and the Combination Problem in Disjoint Theories. [Research Report] RR-8476, INRIA. 2014. ⟨hal-00947088⟩



Record views


Files downloads