氏名: 谷口 貴啓 (089433440)
論文題目: 項書換え系のＡＣ停止性の研究
論文概要
等式論理における自動証明で用いられるKnuth-Bendixアルゴリズムは、
与えられた等式集合をそれと等価な停止性と合流性をもつ項書き換え系
に変換する。
しかし、規則に結合律(Associative)と交換律（Commutative)を含む場合には、
停止性が保証されないため、これらの規則を特別に扱うAC書き換え系が導入された。
AC書き換え系における完備化手続きでは、AC停止性を保証するAC順序の
研究が進められてきた。これらの順序の中で、Kapurの提案した順序は、
整礎性、単調性、AC整合性を満たすが、この順序は、複雑なため解析が容易ではなく、
項の代入に関して安定でないという問題点もある。
本論文ではKapurの順序を実現したプログラムを作成して、
実際に例題を入力しその問題点の原因を研究する。
目次に戻る