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, giving the first unification method for asymmetric unification in the combination of disjoint theories. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Erbatur, S., Kapur, D., Marshall, A. M., Meadows, C., Narendran, P., & Ringeissen, C. (2014). On asymmetric unification and the combination problem in disjoint theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8412 LNCS, pp. 274–288). Springer Verlag. https://doi.org/10.1007/978-3-642-54830-7_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
