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 left-distributivity 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é Paris-Sud,
Orsay, France, April 1992.
- [Con93a]
-
Evelyne Contejean.
A partial solution
for D-unification based on a reduction to AC1-unification.
In Proceedings of the EATCS International Conference on
Automata, Languages and Programming, pages 621–632, Lund, Sweden, July
1993. Springer-Verlag.
- [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 Schmidt-Schauß.
Unification of stratified second-order terms.
Research Report 12/94, Fachbereich Informatik, Universität
Frankfurt, Germany, December 1994.
- [SS97]
-
Manfred Schmidt-Schauß.
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 one-sided distributivity.
Journal of Symbolic
Computation, 3:183–202, 1987.