2021 Fiscal Year Annual Research Report
Inductive thoeorems and ground confluence for conditional term rewriting systems
| Project/Area Number |
18K11158
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | 条件付き項書き換えシステム / 帰納的定理 / 基底合流性 / ホーン節論理 |
|---|
| Outline of Annual Research Achievements |
書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.
本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている.本年度は,前年度に与えたホーン節帰納的定理の改良書き換え帰納法の自動証明手続きを検討し実装システムを構築した。また実装したシステムを用いた計算機実験により、帰納的定理の証明に成功する新たな例を明らかにした。また、条件付き項書き換えシステムの十分完全性の自動検証法および自動検証システムの構築について引き続き研究を進め、異なるアプローチに基づく複数の検証システムを構築し比較実験を行った。
本年度は，前年度採録となっていた論文が出版され，その掲載料を支払った．
|
