氏名: 石井 宏諭 (089433025)

論文題目: 結合律と交換律を法とする書換え系の停止性を保証するための順序の研究


論文概要

等式論理の定理自動証明の手法にKnuth-Bendixの完 備化手続きがある。この手続きでは与えられた等式の 集合から合流性と停止性を満たす項書換え系Rを出力 する。証明すべき等式の両辺についてそれぞれのRに よる正規形が一致すれば、その等式は定理であること が示される。しかしながら、結合律と交換律を持つ論 理の場合には、この手続きは無限ループに陥る。これ は、交換律を持つ項書換え系は停止性を持たないから である。 この欠点を補うために、AC書換えが考案された。こ れは、結合律と交換律(Associative-Commutative) で等しくなる項を同一の項と考えて、項を書き換える システムである。このシステムにおいて、完備化手続 きを行うためには、停止性を保証するための順序が必 要となる。 このシステムの停止性を示すために、Deepak Kapur とG.Sivakumarによって、無限減少列のない順序付け が提案された。それは、AC関数記号に関する項につい て、その項の特徴をあらわすCandidateを求め、これ を既存の方法で比較することにより、2つの項の間の 順序関係を求めるものである。 本論文では、再帰経路順序(Recursive Pass Order )を用いてCandidateを比較し、順序関係を求めるア ルゴリズムを、言語MLを用いて実現し、証明系への応 用を検討する。


目次に戻る


asakura@nuie.nagoya-u.ac.jp