Proof Transformation of Cyclic Proofs

• Project/Area Number: 25K14999
• 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: National Institute of Informatics
• Principal Investigator: 龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• Project Period (FY): 2025-04-01 – 2030-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥6,110,000 (Direct Cost: ¥4,700,000、Indirect Cost: ¥1,410,000); Fiscal Year 2029: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2028: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2027: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2026: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2025: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 循環証明 / 証明論

Outline of Research at the Start

2006年に循環証明体系が帰納的定義を形式化する新しい論理体系として提案され、従来のものより自動証明と対話型証明の両方に優れているため、活発に研究されている。循環証明を普通の証明に変換する証明変換は、循環証明の証明可能性を普通の証明に帰着することができ重要であるが、述語論理に対する既存研究は本申請者のものが世界的にも中心である。本研究は、循環証明体系から普通の証明体系への既存の証明変換を、(1) 直観主義論理、(2) 高階論理、(3) 自然演繹、(4) 型理論に拡張し、これを総合することにより対話型証明システム Coqを循環証明体系に拡張して、さらに実装実験も行う。