Projekt A10 - Unifikation in Gleichheitstheorien

(bis 12/99)

Das Unifikationsproblem einer Gleichheitstheorie E ist das Problem zu entscheiden, ob ein endliches System von Gleichungen in E lösbar ist, und im positiven Fall ein vollständiges Lösungssystem zu bestimmen. Dieses Problem ist i.a. algorithmisch nicht lösbar, selbst wenn die Gleichheitstheorie E durch ein endliches vollständiges Termersetzungssystem beschrieben wird. Einschränkungen für E werden untersucht, die das Unifikationsproblem für E lösbar machen.

Mitarbeiter:

Daniel Dougherty
(Mathematics Department, Wesleyan University, Middletown, CT, USA)

Paliath Narendran
(Department of Computer Science, State University of New York, Albany, NY, USA)

Interne Berichte:

Otto, F., Narendran, P., and Dougherty, D. :
Equational unification, word unification, and 2nd-order equational unification.
Mathematische Schriften Kassel 8/96, Universität-GH Kassel.
published in Theoretical Computer Science in revised form.

Veröffentlichungen:

Otto, F. and Narendran, P. and Dougherty, D.:
Equational unification, word unification, and 2nd-order equational unification
Theoretical Computer Science,1998:1-47.
Narendran, P. and Otto, F. :
The word matching problem is undecidable for finite special string-rewriting systems that are confluent.
In Degano, P.and~Gorrieri, R. and Marchetti-Spaccamela, A., editors, Automata, Languages and Programming, Lecture Notes in Computer Science 1256, pages 638-648. Springer-Verlag 1997, Berlin.
Narendran, P. and Otto, F. :
Single versus simultaneous equational unification and equational unification for variable-permuting theories.
Journal of Automated Reasoning, 1997, 19:87-115.
Otto, F. :
Solvability of word equations modulo finite special and confluent string-rewriting systems is undecidable in general.
Information Processing Letters,1995, 53:237-242.
Otto, F., Narendran, P., and Dougherty, D. :
Some independence results for equational unification.
In Hsiang, J., editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science 914, pages 367-381. Springer-Verlag 1995, Berlin.
Narendran, P. and Otto, F. :
Some results on equational unification.
In Stickel, M., editor, Proceedings 10th CADE, Lecture Notes in Artificial Intelligence 449, pages 276-291. Springer-Verlag 1990, Berlin.
Otto, F. :
On two problems related to cancellativity.
Semigroup Forum, 1986, 33:331-356.