TY  - UNPD
A1  - Schmidt-Schauß, Manfred
T1  - An algorithm for distributive unification
T2  - Universität Frankfurt am Main. Fachbereich Informatik: Interner Bericht ; 94,13
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 2
N2  - We consider unification of terms under the equational theory of two-sided distributivity D with the axioms x*(y+z) = x*y + x*z and (x+y)*z = x*z + y*z. The main result of this paper is that Dunification is decidable by giving a non-deterministic transformation algorithm. The generated unification are: an AC1-problem with linear constant restrictions and a second-order unification problem that can be transformed into a word-unification problem that can be decided using Makanin's algorithm. This solves an open problem in the field of unification. Furthermore it is shown that the word-problem can be decided in polynomial time, hence D-matching is NP-complete.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 2 
T3  - Interner Bericht / Fachbereich Informatik, Johann Wolfgang Goethe-Universität Frankfurt a.M. - 94,13 
Y1  - 1994
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4596
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-8891
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/schauss/DUNI.ps
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -