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)


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
PublisherSpringer Verlag
Number of pages12
ISBN (Print)9783642370632
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


Other7th International Conference on Language and Automata Theory and Applications, LATA 2013


  • Rule-Based Calculi
  • Semi-Unification
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this