形式証明の理論依存性解析とその計算可能証明発見への応用

2013 Fiscal Year Research-status Report

• Project/Area Number: 25540003
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: 数理論理 / 定理証明系 / 古典論理 / 計算的意味

Research Abstract

H25年度は、(1) Open induction に基づく Higman の補題の Isabelle/HOL における形式証明、および (2) 定理証明系 Isabelle/HOL の proof term に関する機能について調査を進めた。
(1) については、Christian Sternagel 博士（2013年11月まで本研究室ポスドク、現インスブルック大学）の協力により、 Higman の補題の minimal bad sequence論法に基づく標準的な証明を Isabelle/HOL上に実装し、さらに2012年10月30日に Isabelle Archaive of Formal Proofs に登録した Open induction のライブラリを用いた証明（Tierry Coquand による1993年の証明）の Isabelle/HOL への実装を試みた。ただし、原証明にはギャップがあり、Alfons Geser による ad hoc な修正が知られているが、現在、open induction の原理の拡張に基づく修正の検討を続けている。
(2) については、博士課程前記学生を雇用し調査したが、学生の定理証明系に対する理解がおよばす頓挫した。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

上記の実績概要にあげた (1) の Tierry Coquand による原証明の修正は開始前より予定していたが、予想以上に微妙な問題（Isabelle/HOL 上のでの形式証明記述上の記号の扱いの問題を含む）があり、手間取った。(2) については、雇用した学生の能力が及ばす（定理証明系の習得には通常、最低３か月程度は要し、使いこなしは数学的な証明力に依存する）、H26年度に研究代表者自身が進める予定である。このため、ミュンヘン大学、スワンジー大学などとのインフォーマルな討論や研究交流は行ったが、論文発表や学会発表等には至らなかった。

Strategy for Future Research Activity

Open induction原理がそのままではHigmanの補題の証明が不自然な順序を用いることになるため、原理の拡張が必要と考えている。その検討をスワンジー大学 Ulrich Berger 博士、Monika Seisenberg 博士らの協力を得て進め、Isabelle/HOL上の形式証明ライブラリとして Higmanの補題の open induction による証明と合わせて実装をめざす。Higman の補題の次のターゲットとして、FP7のプロジェクトである CCC (Continuity, Computability, Constructivity) と連携して、Lovasz の補題など、連続的な性質の証明の構造の調査および計算可能な証明について検討を進める。
また、Isabelle/HOL における proof term に関する調査は、インスブルック大学 Christian Stenagel 博士の協力を得て、研究代表者が進める。