| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,ソフトウェアの正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかし,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,TRSにおける最も基本的で重要な問題である合流性及び単一化問題について研究を行い,前年度に得られた結果をさらに拡張すると共に,その研究成果に基づくより強力な拡張危険対の新しい完備化法を明らかにした.即ち,まず,強い探さ保存性を満たす右線形TRSに関する前年度の結果を拡張して,合流性を保証する,より一般的な条件を明らかにすると共に,この条件に基づく,制限のない任意のTRSに対して適用可能な完備化法を明らかにした.さらに,これらの研究成果を基盤とする,新しい定理の自動証明システムの設計方針を確立し,そのプロトタイプを実装した.次に,線形TRSの合流性に関する従来の結果をさらに拡張すると共に,TRSの部分(sub)TRSの合流性が既知の場合に,元のTRS全体の合流性を保証するためのより一般的な条件を明らかにした.さらに,合流性を満たす右定項TRSの単一化問題の可解性を明らかにした.この研究成果はこの分野で最も権威のある雑誌の一つであるInformation and Computationに掲載が決定された.また,合流性をみたす右定項TRSを真に含む幾つかのクラスについては単一化問題が非可解であることも明らかにした.
以上より,本年度は学術的に重要な研究成果を得ると共に,次年度の新しい定理の自動証明法の確立及びその実現に必須な準備研究を行い,所期の目標を達成することができた.
|
