氏名: 河井 規浩 (089433211)
論文題目: 項集合書き換え系の実現
論文概要
項書換え系（TRS）に基づくKnuth-Bendixアルゴリズムによる完備化は、
等式論理における自動証明法として有望である。
このアルゴリズムは失敗する場合もあるため、そのような場合も証明を
続けることを目的として項集合書換え系（TSRS）が提案された。
TSRSとは、TRSの書き換え規則の両辺を
項の集合に拡張し、項の集合を書き換えるシステムである。
これまでに、単純なTSRSについては合流条件が知られており、完備化への応用が
可能であると考えられている。
しかし、実際に動くシステムが作られていないため、
その実用性については議論できない状況にある。
本論文では、一般のTSRS、単純なTSRSのそれぞれを実現し、
それに関する問題点について論じる。
目次に戻る