| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,ソフトウェアの正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかし,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,TRSにおける最も基本的で重要な問題である合流性及び単一化問題について研究を行い,前年度に得られた結果をさらに拡張する結果を得た.まず,単一化問題に関して,従来得られていた結果を拡張して,合流性を満たす単純TRSのクラスにおいてもこの問題が可解であることを示すと共に,合流性及び停止性を満たす単項的線形TRSのクラスにおいては決定不能であることを明らかにした.次に,合流性問題に関して,書き換え系列の概念を拡張した書き換えグラフの概念を用いて,従来の結果を真に拡張する結果を得ると共に,TRSが階層構造化され,その部分(sub)TRSの合流性が既知の場合において,TRS全体の合流性を保証する,より一般的な条件を明らかにした.さらに,TRSの停止性を前提にするという従来の定理の自動証明法とは異なり,停止性などの条件を必要としない,より一般的な広いクラスを対象とする新しい定理の自動証明法を初めて明らかにした.また,終代数に基づく定理の自動証明法についての理論的基礎を確立し,この枠組の中で強完全性を保証する,より一般的な条件を明らかにすると共に,新しい定理の自動証明システムを計算機上に実現して,種々の実現上の問題点を洗い出し,その解決のための改善を行った.
以上のことより、本年度の研究計画の所期の目的を達成することができた.なお,本年度は本研究課題の最終年度に当り,これらの研究成果をまとめ,報告書を作成した.
|
