On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)

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. 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 an overview of a new formulation of the method for unification in the combination of disjoint equational theories developed by Baader and Schulz that gives a new unification method for asymmetric unification in the combination of disjoint theories.