A universal unification algorithm based on unification-driven leftmost outermost narrowing

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: etn-tra). For a ctn-tra R and for two terms t and s, the algorithm computes a ground-complete...

Full description

Saved in:
Bibliographic Details
Main Authors: Fassbender Heinz
Vogler Heiko
Format: Article
Published: 1994
Series:Acta cybernetica 11 No. 3
Kulcsszavak:Számítástechnika, Kibernetika
Subjects:
Online Access:http://acta.bibl.u-szeged.hu/12526
Description
Summary: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: etn-tra). For a ctn-tra R and for two terms t and s, the algorithm computes a ground-complete set of (Ez, A)-unifiers of t and s, where Ez is the set of rewrite rules of R viewed as equations and A is the set of constructor symbols. 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 interleaves leftmost outermost narrowing steps with decomposition steps taken from the usual unification of terms. In its turn, every decomposition step involves a consistency check on constructor symbols combined with a particular form of the occur check. Since decomposition steps are performed as early as possible, some of the nonsuccessful derivations can be stopped earlier than in other universal unification algorithms for ctn-trs's. We give a proof that our algorithm really is a universal unification algorithm.
Physical Description:139-167
ISSN:0324-721X