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

2001 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の単一化問題の可解性を明らかにした.この研究成果はこの分野で最も権威のある雑誌の一つであるInformation and Computationに掲載が決定された.また,合流性をみたす右定項TRSを真に含む幾つかのクラスについては単一化問題が非可解であることも明らかにした.
以上より,本年度は学術的に重要な研究成果を得ると共に,次年度の新しい定理の自動証明法の確立及びその実現に必須な準備研究を行い,所期の目標を達成することができた.

Research Products

• [Publications] TOYAMA, Y.: "Conditional Linearization of Non-Duplicating Term Rewriting Systems"IEICE Trans.Inf.& Syst.. E84-D・4. 439-447 (2001)
• [Publications] OYAMAGUCHI, M.: "The Unification Problem for Confluent Right-Ground Term Rewriting Systems"Proc.12th Rewriting Techniques and Applications Lecture Notes in Computer Science. 2051. 246-260 (2001)
• [Publications] OYAMAGUCHI, M.: "An E-critical Pair Completion Procedure for Nonterminating TRS's and its Application"Proc.International Workshop on Rewriting in Proof and Computation. 208-215 (2001)
• [Publications] OYAMAGUCHI, M.: "The Unification Problem for Confluent Right-Ground Term Rewriting Systems"Information and Computation. (掲載決定). (2002)