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
Solving *-problems modulo Distributivity by a Reduction to AC1-unification

Solving *-problems modulo Distributivity by a Reduction to AC1-unification

Evelyne Contejean

Abstract

We show that unification modulo both-sided distributivity of the symbol * on + can be reduced to AC1-unification for all unification problems which do not involve the + operator. Moreover, in this case, we can describe ``almost all'' solutions in a finite way, although there are in general infinitely many minimal solutions for such problems.
full paper