書き換えシステムの基本的性質の解明と定理の自動証明に関する研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12680344
• Research Institution: Mie University
• Principal Investigator: 大山口 通夫 三重大学, 工学部, 教授 (50111828)
• Keywords: 項書き換えシステム / Church-Rosser(合流性) / 非線形TRS / 完備化手続き / 定理の自動証明 / 単一化 / 深さ保存性 / 拡張危険対の完備化

Research Abstract

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

Research Products

• [Publications] TOYAMA,Y.: "Conditional Linearization of Non-Duplicating Term Rewriting Systems"IEICE Trans.Inf. & Syst.. (掲載決定). (2001)
• [Publications] OYAMAGUCHI,M.: "The Unification Problem for Confluent Right-Ground Term Rewriting Systems"Proc.12th Rewriting Techniques and Applications. (掲載決定). (2001)