コンピュータによる定理証明支援とその応用
| 整理番号 | 2024a024 |
|---|---|
| 種別 | プロジェクト研究-短期共同研究 |
| 研究計画題目 | コンピュータによる定理証明支援とその応用 |
| 研究代表者 | Jacques Garrigue（名古屋大学多元数理科学研究科・教授） |
| 研究実施期間 |
2024年11月25日(月) ～
2024年11月26日(火) |
| 研究分野のキーワード | 定理証明支援系、形式論理、型理論、高階論理、プログラミング言語理論、アルゴリズム論、形式証明 |
| 本研究で得られた成果の概要 | この短期共同研究は元々、定理証明および定理証明支援系の研究者を集め、現状を確認し、今後の研究の方向性を提示するために計画された。この分野の多数の研究者が集まり、自分の経験をもとに様々な研究結果を発表し合った。Pédrot氏の講演などでは、強固な論理基盤を守りながら定理証明支援系を実装することの難しさが共有できた。また、それぞれの分野での定理証明の応用を通じて、形式証明の利用が現実的になっていることも再確認できた。中でも、定理証明支援系による論理学や数学基礎論に関する証明が多く紹介され、この分野の基盤強化に貢献できた。議事録はMIレクチャーノートとして出版予定である。また、来年も同様の集まりを東北大学で開き、研究の継続推進を図る予定である。 |
| 組織委員(研究集会) 参加者(短期共同利用) |
GARRIGUE Jacques（名古屋大学多元数理科学研究科・教授） 南出靖彦（東京工業大学情報理工学院数理・計算科学系・教授） 中正和久（山口大学工学部知能情報工学科・准教授） |