循環証明の証明変換

• 研究課題/領域番号: 25K14999
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 国立情報学研究所
• 研究代表者: 龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• 研究期間 (年度): 2025-04-01 – 2030-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 6,110千円 (直接経費: 4,700千円、間接経費: 1,410千円); 2029年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2028年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2027年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2026年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2025年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
• キーワード: 循環証明 / 証明論

研究開始時の研究の概要

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