氏名: 亀井 政史 (l0351626)
論文題目: メタ項書換え計算によるKnuth-Bendixアルゴリズムの実現
論文概要
メタ項書換え計算（MRC）は、項書換え系の変換アルゴリズムなどの記述・実
行・解析を目的とした計算モデルであり、規則や項書換え系をFirst Class
Objectとして扱うことができる。一方、Knuth-Bendix完備化アルゴリズムは
（停止性はあるが）合流性のない項書換え系（TRS）を合流性のあるTRSに変換
する手続きである。合流性は、定理自動証明にTRSを用いるとき、そのTRSに要求
される最も重要な性質である。
本研究では、Knuth-Bendix完備化アルゴリズムをMRCで実現する手法を検討し、
MRCの表現能力を評価するとともに、KBアルゴリズム、あるいは、その他のTRS
の変換アルゴリズムの解析に、MRCの解析技法を利用する際の問題点を明らか
にする。
目次に戻る