モデル生成器を利用した条件付き項書き換えシステムの合流性検証に関する研究

Research Project

Project/Area Number	24K14817
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60010:Theory of informatics-related
Research Institution	Niigata University
Principal Investigator	青戸等人新潟大学, 自然科学系, 教授 (00293390)
Project Period (FY)	2024-04-01 – 2027-03-31
Project Status	Granted (Fiscal Year 2024)
Budget Amount *help	¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000) Fiscal Year 2026: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000) Fiscal Year 2025: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000) Fiscal Year 2024: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Keywords	項書き換えシステム / 合流性 / 条件付き項書き換えシステム / モデル生成器
Outline of Research at the Start	条件付き項書き換えシステムは，ホーン節理論に対応する書き換えシステムの拡張であり，より広範な代数構造を対象とするばかりでなく，関数型プログラムのより直接的な翻訳を実現できるため，応用上も重要な拡張である．条件付き項書き換えシステムの合流性検証では，従来の書き換え理論の様々な応用を用いた合流性検証ツールと第一階述語論理の定理自動証明ツールを用いるアプローチに基づく合流性検証ツールが拮抗している．本研究では，2 つのアプローチをどのように融合できるか，また，それによって，より強力な条件付き項書き換えシステムの強力な検証法を実現できるかを検討する．