首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:正則項上の単一化について
  • 本地全文:下载
  • 作者:岩見 宗弘
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2018
  • 卷号:35
  • 期号:4
  • 页码:151-163
  • DOI:10.11309/jssst.35.151
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    有限項に対する(一階の)単一化アルゴリズムは推論規則を用いて形式化され,その停止性,健全性と完全性が多くの文献で示されている.また,いくつかの先行研究において,正則項に対する単一化アルゴリズムも推論規則を用いて与えられている.しかしながら,それらの研究において,与えられた等式集合から推論規則により得られた集合の解ともとの集合の最汎単一化子である正則代入が一致することは明確に示されていない.また,停止性,健全性と完全性の明確な証明を与えているものはない.本論文では,正則項に対する単一化アルゴリズムの基礎理論を項書換えシステムの枠組みで整理し直すことを目標とする.まず,再帰式表現の解はその再帰式表現に対応する等式集合の最汎単一化子であることを示す.次に,正則項に対する単一化アルゴリズムを推論規則を用いて再定式化し,その停止性,健全性と完全性の明確な証明を示す.最後に,単一化可能な等式集合は正則代入で表現される最汎単一化子をもつことの完全な証明を与える.

国家哲学社会科学文献中心版权所有