|
項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た：（１）可換性分解、危険対解析、Ｅ単一化に関する技法を開発・発展させ、強力な合流性解析を実現した。（２）それらの知見の応用として、定理自動証明の基盤理論である抽象完備化の正当性についての簡潔な証明、（３）さらに計算を効率的に行うための基本正規化定理を得た。
|
