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ß  and Baader-Schulz  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
This document was translated from LATEX by HEVEA.