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...
Elmentve itt :
| Szerzők: | |
|---|---|
| Dokumentumtípus: | Cikk |
| Megjelent: |
1994
|
| Sorozat: | Acta cybernetica
11 No. 3 |
| Kulcsszavak: | Számítástechnika, Kibernetika |
| Tárgyszavak: | |
| Online Access: | http://acta.bibl.u-szeged.hu/12526 |
| Tartalmi 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. |
|---|---|
| Terjedelem/Fizikai jellemzők: | 139-167 |
| ISSN: | 0324-721X |