項書換系の技術の定理証明支援系への応用

• Project/Area Number: 24K20758
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60050:Software-related
• Research Institution: Kyoto University
• Principal Investigator: 池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
• Project Period (FY): 2024-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2028: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2027: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2025: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: 定理証明支援系 / 項書換え系

Outline of Research at the Start

定理証明支援系とは，プログラム等についての数学的性質とその証明をコンピュータ言語で記述できるようなソフトウェアシステムである．記述された証明の正しさはシステムにより機械的にチェックされるため，プログラムが仕様通りに動作するか等の保証を与える手法の一つとして注目されている．しかし，複雑な証明を人間が考え記述しなければいけないという問題点がある．
本研究では，証明の難しさを緩和するために項書換系の理論を応用し，Coqにプラグインとして実装することで証明の部分的な自動化を図る．