[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

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.


This theory is decidable [SS94][SS97].


Evelyne Contejean. Eléments pour la Décidabilité de l’Unification modulo la Distributivité. PhD thesis, Université Paris-Sud, Orsay, France, April 1992.
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.
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.
Manfred Schmidt-Schauß. Unification of stratified second-order terms. Research Report 12/94, Fachbereich Informatik, Universität Frankfurt, Germany, December 1994.
Manfred Schmidt-Schauß. A unification algorithm for distributivity and a multiplicative unit. Journal of Symbolic Computation, 22(3):315–344, 1997.
Erik Tiden and Stefan Arnborg. Unification problems with one-sided distributivity. Journal of Symbolic Computation, 3:183–202, 1987.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]