コンピュータによる定理証明支援とその応用

整理番号	2024a024
種別	プロジェクト研究-短期共同研究
研究計画題目	コンピュータによる定理証明支援とその応用
研究代表者	Jacques Garrigue（名古屋大学多元数理科学研究科・教授）
研究実施期間	2024年11月25日(月) ～ 2024年11月26日(火)
研究分野のキーワード	定理証明支援系、形式論理、型理論、高階論理、プログラミング言語理論、アルゴリズム論、形式証明
目的と期待される成果	（１）社会における証明の必要性が増大し続けている。様々なインフラを支えるアルゴリズムにおいて、実装のバグが致命的な結果に至る危険性があり、金融などにおいて損害が兆単位になることもありうる。また、実装以前に、アルゴリズムの元となっている数学も正しくなければならない。 （２）定理証明支援系は元々論理のステップを確認するために作られたツールであるが、プログラムの証明と数学の証明の両方が確認でき、完全な安全性を確保するただ一つの手法とも言える。定理証明器ではなく、定理証明支援系が必須な理由は、TuringがEntscheidungsproblemを否定したことで、人間を介さずにコンピューターのみで全ての証明を構築することが不可能だからである。 （３）この研究計画では、様々な定理証明支援系の開発者と利用者を集めて研究集会を行う予定である。それによる相乗効果で、この分野を活性化する。対象分野はプログラミング言語、アルゴリズム、純粋数学や応用数学など、広く集める。また、定理証明支援系の種類も指定せず、お互いにアイデアを出し合える場とする。 （４）この分野において長年続いて来たTPPという研究集会の過去の開催者の協力を得て、今年は20回目のTPPを九州大学で開催することを目指す。TPPでは毎年50人前後が集まるが、節目の年でそれより多く集まりそうだ。また、海外から研究者を招聘し、交流を増やす予定である。
組織委員(研究集会) 参加者(短期共同利用)	GARRIGUE Jacques （名古屋大学多元数理科学研究科 ・教授 ） 南出靖彦 （東京工業大学情報理工学院数理・計算科学系 ・教授 ） 中正和久 （山口大学工学部知能情報工学科 ・准教授 ）