A universal unification algorithm based on unification-driven leftmost outermost narrowing
FakultätFakultät für Ingenieurwissenschaften und Informatik
Ressourcen- / MedientypArbeitspapier, Text
Datum der Freischaltung2009-08-09
We formalize a universal unification algorithm for the class of equational theories which is induced by the class of canonical, totally-defined, not strictly subunifiable term rewriting systems (for short: ctn-trs). For a ctn-trs R and for two terms t and s, the algorithm computes a ground-complete set of E_R-unifiers of t and s, where E_R is the set of rewrite rules of R viewed as equations. The algorithm is based on the unification-driven leftmost outermost narrowing relation (for short: ulo narrowing relation) which is introduced in this paper. The ulo narrowing relation combines usual leftmost outermost narrowing steps and unification steps. Since the unification steps are applied as early as possible, some of the nonsuccessful derivations can be stopped earlier than in other approaches to E_R-unification. Furthermore, we formalize a deterministic version of our universal unification algorithm that is based on a depth-first left-to-right traversal through the narrowing trees.
LizenzStandard (Fassung vom 01.10.2008)
Rewriting systems (Computer science)