Fassbender Heinz; Vogler Heiko: A universal unification algorithm based on unification-driven leftmost outermost narrowing. In: Acta cybernetica, (11) 3. pp. 139-167. (1994)
Előnézet |
Cikk, tanulmány, mű
cybernetica_011_numb_003_139-167.pdf Letöltés (1MB) | Előnézet |
Absztrakt (kivonat)
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.
| Mű típusa: | Cikk, tanulmány, mű |
|---|---|
| Befoglaló folyóirat/kiadvány címe: | Acta cybernetica |
| Dátum: | 1994 |
| Kötet: | 11 |
| Szám: | 3 |
| ISSN: | 0324-721X |
| Oldalak: | pp. 139-167 |
| Nyelv: | angol |
| Kiadás helye: | Szeged |
| Befoglaló mű URL: | http://acta.bibl.u-szeged.hu/38497/ |
| Kulcsszavak: | Számítástechnika, Kibernetika |
| Megjegyzések: | Bibliogr.: p. 166-167. ; összefoglalás angol nyelven |
| Szakterület: | 01. Természettudományok 01. Természettudományok > 01.02. Számítás- és információtudomány |
| Feltöltés dátuma: | 2016. okt. 15. 12:26 |
| Utolsó módosítás: | 2022. jún. 13. 11:29 |
| URI: | http://acta.bibl.u-szeged.hu/id/eprint/12526 |
 |
Tétel nézet |
