Problem #38 (Solved !)
Originator: Jörg Siekmann
Date: April 1991
Summary:
Is unification modulo distributivity decidable?
Is satisfiability of equations in the theory of distributivity (unification
modulo modulo one right and one leftdistributivity axiom) decidable? (With
just one of these, the problem had already been solved in [TA87].)
A partial positive solution is given in [Con93a], based on a
striking result on the structure of certain proofs modulo distributivity.
Although many more cases are described in
[Con92][Con93b], the general case remains open.
Remark
This theory is decidable [SS94][SS97].
References

[Con92]

Evelyne Contejean.
Eléments pour la Décidabilité de l’Unification
modulo la Distributivité.
PhD thesis, Université ParisSud,
Orsay, France, April 1992.
 [Con93a]

Evelyne Contejean.
A partial solution
for Dunification based on a reduction to AC1unification.
In Proceedings of the EATCS International Conference on
Automata, Languages and Programming, pages 621–632, Lund, Sweden, July
1993. SpringerVerlag.
 [Con93b]

Evelyne Contejean.
Solving linear
Diophantine constraints incrementally.
In David S. Warren, editor, Proceedings of the Tenth
International Conference on Logic Programming, Logic Programming, pages
532–549, Budapest, Hungary, June 1993. The
MIT Press.
 [SS94]

Manfred SchmidtSchauß.
Unification of stratified secondorder terms.
Research Report 12/94, Fachbereich Informatik, Universität
Frankfurt, Germany, December 1994.
 [SS97]

Manfred SchmidtSchauß.
A unification algorithm for distributivity and a multiplicative unit.
Journal of Symbolic
Computation, 22(3):315–344, 1997.
 [TA87]

Erik Tiden and Stefan Arnborg.
Unification problems with onesided distributivity.
Journal of Symbolic
Computation, 3:183–202, 1987.