| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,プログラムの仕様と実現の正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,TRSにおける最も基本的で重要な問題である合流性及び単一化問題について研究を行い,判定可能なより広いクラスを明らかにすると共に,その研究成果に基づく(拡張)危険対の新しい完備化法を明らかにした.即ち,まず,強い深さ保存性を満たす右線形TRSについて,その合流性を保証する,より一般的な条件を明らかにすると共に,この条件に基づく,制限のない任意のTRSに対して適用可能な完備化法を明らかにした.次に,線形TRSの合流性に関する,長い間未解決であった重要な問題について研究を行い,従来の結果をさらに拡張することに成功した.また,TRSの部分(sub)TRSの合流性が既知の場合に,元のTRS全体の合流性を保証するためのより一般的な条件を明らかにした.さらに,合流性を満たす右定項TRSの単一化問題の可解性を新しい証明手法を導入することにより,明らかにした.この研究成果はこの分野で最も権威のある国際会議(RTA)で発表論文として採択された.
以上のことより,本年度は学術的に重要な研究成果を得ると共に,次年度以降の新しい定理の自動証明法の実現に必須な準備研究を行い,所期の目標を達成することができた.
|
