Termination of rule-based calculi for uniform semi-unification

Takahito Aoto, Munehiro Iwami

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Uniform semi-unification is a generalization of unification; its efficient algorithms have been extensively studied in (Kapur et al., 1994) and (Oliart&Snyder, 2004). For (uniform) semi-unification, several variants of rule-based calculi are known. But, some of these calculi in the literature lack the termination property, i.e. not all derivations are terminating. We revisit symbolic semi-unification whose solvability coincides with that of uniform semi-unification. We give an abstract criterion of the strategy on which a general rule-based calculus for symbolic semi-unification terminates. Based on this, we give an alternative and robust correctness proof of a rule-based uniform semi-unification algorithm.

Original languageEnglish
Title of host publicationLanguage and Automata Theory and Applications - 7th International Conference, LATA 2013, Proceedings
Pages56-67
Number of pages12
DOIs
Publication statusPublished - 2013
Event7th International Conference on Language and Automata Theory and Applications, LATA 2013 - Bilbao, Spain
Duration: 2013 Apr 22013 Apr 5

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7810 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Conference on Language and Automata Theory and Applications, LATA 2013
CountrySpain
CityBilbao
Period13/4/213/4/5

Keywords

  • Rule-Based Calculi
  • Semi-Unification
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Termination of rule-based calculi for uniform semi-unification'. Together they form a unique fingerprint.

  • Cite this

    Aoto, T., & Iwami, M. (2013). Termination of rule-based calculi for uniform semi-unification. In Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Proceedings (pp. 56-67). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7810 LNCS). https://doi.org/10.1007/978-3-642-37064-9-7