| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,ソフトウェアの正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,TRSの停止性が保証されない場合,或いはTRSが非線形である場合についてはまだ多くの重要な問題が未解決のまま残されていた.そこで,本研究では,まず,非停止または非線形TRSの合流性に関する未解決問題について考察し,新しい証明手法を考案することにより,従来の結果を真に拡張すると共に,従来得られていた,左線形TRSの合流性を保証する条件を一般化することに成功した.次に,以下の条件(a)〜(c)を満たすTRSの部分クラスSが存在することを明らかにした.
(a)任意のTRSから部分クラスSのあるTRSへ等価性(合同関係)を保存した変換手続きが存在し,(b)部分クラスSの書き換えによる計算能力はTuring機械(一般のプログラム)の計算能力と同等で,(c)部分クラスSにおいて,完備化手続きが構築できるような,合流性を保証する条件が導き出せること.
さらに,クラスSの合流性を保証する条件からTRSの完備化手続きを構成し,この完備化手続きに基づく定理の自動証明法についての理論的基礎を確立すると共に,新しい定理の自動証明システムを実現して,その有用性を実証した.
本研究では,TRSの最も重要な問題の一つである単一化問題についても考察し,合流性を満たす右定項TRSの単一化問題が可解であることを明らかにした.さらに,この証明手法を拡張して合流性を満たす単純TRSの単一化問題が可解であることを示すと共に,合流性を満たす単項TRSについてはこの問題が非可解であることを示した.
|
