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.
CITATION STYLE
Contejean, E. (1993). A partial solution for D-unification based on a reduction to AC1-unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 700 LNCS, pp. 621–632). Springer Verlag. https://doi.org/10.1007/3-540-56939-1_107
Mendeley helps you to discover research relevant for your work.