| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,ソフトウェアの正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかし,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,研究の最も遅れている非線形TRSのクラスにおける基本的で重要な問題について研究を行い,幾つかの新しい結果を得ることに成功した.即ち,まず準構成子TRSのクラス(SC)においては,線形性又は単項性を仮定しても,ほとんど全ての判定問題が非可解であることを示した.特に,注目すべき結果は合流性問題及び単一化問題が単項的なクラスSCにおいて非可解であることを示したことである.次に,本研究では,合流性を満たすクラスSCについて考察し,項合流性問題,語問題及び単一化問題が可解であることを示すと共に,到達可能性問題については非可解であることを明らかにした.これまで,項合流性問題と到達可能性問題は同程度に難しい問題と考えられており,TRSの種々の部分クラスにおいて,共に非可解であるか又は共に可解であるという結果のみが得られていたが,本研究の結果はこの従来の常識を覆す初めての結果であり,注目すべきものである.また,本研究では,合流を満たすクラスSCにおいて,到達可能性が判定可能となるための十分条件を幾つか明らかにした.さらに,本研究では終代数に基づく定理の自動証明法について研究し,その理論的基礎を確立すると共に,その応用例として左線形非停止TRSのクラスにおける定理の自動証明システムを提示し,その有用性を明らかにした.
|
