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

Fassbender Heinz and Vogler Heiko: A universal unification algorithm based on unification-driven leftmost outermost narrowing. In: Acta cybernetica, (11) 3. pp. 139-167. (1994)

[thumbnail of cybernetica_011_numb_003_139-167.pdf]
Cikk, tanulmány, mű

Download (1MB) | Preview


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.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 1994
Volume: 11
Number: 3
ISSN: 0324-721X
Page Range: pp. 139-167
Language: English
Place of Publication: Szeged
Related URLs: http://acta.bibl.u-szeged.hu/38497/
Uncontrolled Keywords: Számítástechnika, Kibernetika
Additional Information: Bibliogr.: p. 166-167. ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2016. Oct. 15. 12:26
Last Modified: 2022. Jun. 13. 11:29
URI: http://acta.bibl.u-szeged.hu/id/eprint/12526

Actions (login required)

View Item View Item