ohne Drittmittelfinanzierung
Unifikation in Gleichheitstheorien
Details zum Projekt
Projektlaufzeit: 10/1989–06/1999
Webseite: http://elba.db.informatik.uni-kassel.de/FG_TH/projekte/proj02.html
Zusammenfassung
Das Unifikationsproblem einer Gleichheitstheorie E ist das Problem
zu entscheiden, ob ein endliches System von Gleichungen in E loesbar
ist, und im positiven Fall ein vollstaendiges Loesungssystem zu
bestimmen. Dieses Problem ist i.a. algorithmisch nicht loesbar,
selbst wenn die Gleichheitstheorie E durch ein endliches vollstaendiges
Termersetzungssystem beschrieben wird. Einschraenkungen fuer E werden
untersucht, die das Unifikationsproblem fuer E loesbar machen.