Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Combining Pattern E-unification Algorithms
Combining Pattern E-unification Algorithms
Alexandre Boudet and Evelyne Contejean
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-Schauss 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