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 A partial solution for D-unification based on a reduction to
AC1-unification
A partial solution for D-unification based on a reduction to
AC1-unification
Evelyne Contejean
Abstract
We show that deciding unification modulo both-sided
distributivity of a symbol * over a symbol + can be reduced to
AC1-unification for all unification problems which do not involve
the + operator. Moreover, we can describe ``almost all'' solutions
in a finite way, although there are in general infinitely many minimal
solutions for such problems. As a consequence, *-problems appear as
a good candidate for a notion of solved-form for D-unification. full paper