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

2003 Fiscal Year Annual Research Report

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

Research Abstract

項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,ソフトウ手アの正当性検証など非常に重要な問題を包含していることから、これまで多くの研究者の注目を集め,盛んに研究されてきた.しかし,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,TRSにおける最も基本的で重要な問題である語問題及び単一化問題について研究を行い,これまでに得られた結果をさらに拡張する結果を得た.即ち,まず,単項的TRSのクラスにおいては,停止性,線形性及び合流性を満たす場合においても単一化問題は非可解であるが,合流性を満たす単純TRSのクラスにおいては可解であることを明らかにした.次に,単純TRSのクラスを真に包含する準構成子TRSのクラス(SC)を導入して,合流性を満たすクラスSCの語問題及び単一化問題が可解であることを明らかにした.これらの結果は従来の結果を真に拡張すると共に,TRSの右線形性を仮定しないという点で,全く新しいもめであり,新しいアイデアに基づく証明手法及びより一般化された判定アルゴリズムを考案することにより得られたものである.次に,合流性を満たさないクラスSCにおいては,単一化問題及び項合流性問題が非可解であることを明らかにし,問題の可解なクラスと非可解なクラスの隔たりを埋める研究を行った.さらに,合流性に関する解決問題について研究を行い,合流性を保証するより一般的な条件を明らかにした.また,TRSの停止性を前提としない,完備化法(合流性を満たすTRSへ変換する方法)及び終代数に基づく定理の自動証明法について考察し,従来の結果をさらに一般化すると共に,定理の自動証明システムの問題点を洗い出し,その解決のための改善を行った.

Research Products

• [Publications] OYAMAGUCHI, M.: "The Unification Problem for Confluent Right-Ground Term Rewriting Systems"Information and Computation. 183・2. 187-211 (2003)
• [Publications] OYAMAGUCHI, M.: "On the Open Problems Concerning Church-Rosser of Left-Linear Term Rewriting Systems"IEICE Trans.Inf.& Syst.. E87-D・2. 290-298 (2004)
• [Publications] MITSUHASHI, I.: "The Joinability and Unification Problems for Confluent Semi-Constructor TRSs"Proc.15th Rewriting Techniques and Application. (掲載決定). (2004)