Combining Pattern E-unification Algorithms

Alexandre Boudet and Evelyne Contejean

Abstract: We present an algorithm for unification of higher-order patterns modulo combinations of disjoint first-order equational theories. This algorithm is highly non-deterministic, in the spirit of those by Schmidt-Schauß [2] and Baader-Schulz [1] in the first-order case. We redefine the properties required for elementary pattern unification algorithms of pure problems in this context, then we show that some theories of interest have elementary unification algorithms fitting our requirements. This provides a unification algorithm for patterns modulo the combination of theories such as the free theory, commutativity, one-sided distributivity, associativity-commutativity and some of its extensions, including Abelian groups.

Keywords. Combination of unification algorithms – Pattern equational unification


F. Baader and K. Schulz. Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. Journal of Symbolic Computation, 21(2), Feb. 1996.
M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation, 1990. Special issue on Unification.

Full PaperSlides

This document was translated from LATEX by HEVEA.