Termination of rule-based calculi for uniform semi-unification

Takahito Aoto, Munehiro Iwami

研究成果: Conference contribution

1 被引用数 (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.

本文言語English
ホスト出版物のタイトルLanguage and Automata Theory and Applications - 7th International Conference, LATA 2013, Proceedings
ページ56-67
ページ数12
DOI
出版ステータスPublished - 2013
イベント7th International Conference on Language and Automata Theory and Applications, LATA 2013 - Bilbao, Spain
継続期間: 2013 4 22013 4 5

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
7810 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「Termination of rule-based calculi for uniform semi-unification」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル