| Research Abstract |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,ソフトウェアの正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかし,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,研究の最も遅れている右非線形TRSのクラスにおける基本的で重要な問題について研究を行い,幾つかの新しい結果を得ることに成功した.即ち,準構成子TRSのクラス(SC)においては,線形性又は単項性を仮定しても,ほとんど全ての判定問題が非可解であるのに対して,合流性を満たすクラスSCでは,項合流性問題,語問題及び単一化問題が可解であることを示すと共に,到達可能性問題については非可解であることを明らかにした.また,合流を満たすクラスSCにおいて,到達可能性が判定可能となるための十分条件を幾つか明らかにした.さらに,フラットTRSのクラスにおける到達可能性,項合流性及び合流性判定問題の非可解性を主張したF.Jacquemardの論文において,そのすべての問題に対して,証明に誤りがあることを指摘すると共に,その正しい証明を与えることに成功した.定理の自動証明法に関する研究では,まず高階関数の取り扱いをも可能とする,終代数に基づく定理証明の基礎理論を確立すると共に,その証明システムの実装及び高度化を達成した.さらに,暗号プロトコルの正当性検証などへの応用研究を行い,その有用性を明らかにした.
本年度は本研究課題の最終年度に当り,これらの研究成果をまとめ報告書を作成した.
|
