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)

Preview |
Cikk, tanulmány, mű
cybernetica_011_numb_003_139-167.pdf Download (1MB) | Preview |

## Abstract

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 |