証明アニメーション(構成的プログラミングによる証明テスト技法)

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10480063
• Research Category: Grant-in-Aid for Scientific Research (B)
• Research Institution: Kobe University
• Principal Investigator: 林 晋 神戸大学, 工学部, 教授 (40156443)
• Co-Investigator(Kenkyū-buntansha): 佐藤 雅彦 京都大学, 大学院工学研究科, 教授 (20027387) ; 八杉 満利子 京都産業大学, 理学部, 教授 (90022277) ; 田村 直之 神戸大学, 工学部, 助教授 (60207248)
• Keywords: 形式的証明の開発 / 定理証明 / 論理情報の視覚化 / 古典論理証明の実行 / Curry-Howardの対応

Research Abstract

本年度は,Proof Animation(以下PA)の基本コンセプトの洗練化とモデル化を行い、支援システムProofWorks,ProofWorks-Classicsの実装とそれ上の実験を行った。
構成的数学用の支援システムproofWorksは、証明記述・構築モジュール、プログラム抽出モジュールが完成した。また、これを元にETL小方の理論による古典数学用システムProofWorks-Classicsを実装した。ProofWorks-Classicsは、証明記述・構築、プログラム抽出が古典論理化され、さらにProofWorksに欠けているプログラムの実行系も実装された。ProofWorksでは、証明とプログラムが有機的に結合されているが、Classicsでは、これは未完成である。ProofWorks-classicsでは、線形論理に基づく古典論理系がつかわれている。
PAの基本コンセプトの洗練化としては、PAを定義、定理、推論の各アニメーションに分類し、その条件を検証した。数学的帰納法を使うと、有限個の碁石は常に同色であることを証明できる(ように見える)という、数理パズルを使ってケーススタディを行った。この特定の問題に対してJAVA appletによりPAの視覚化を行い、さらに、同問題をProofWorks,ProofWorks-Classicsにより形式化し、プログラムの抽出と実行による証明のトレースの実験を行った。この実験や先に述べたアプレットを検討した結果、問題の視覚化により抽出されたプログラムを見ることなく、証明のバグを発見できることが判明した。これは予想しなかった成果であり、来年度以降主要な研究テーマとする予定。また、八杉らが計算可能解析学の研究中で提出したガウス関数の例が、PAに面白い例を提供し、さらに、この場合のようなサーチ原理を元に構成的PAを古典化するという方法をCoq project Paulin教授より示唆された。これらを統合して、non-trivialなPAのケーススタディを目指したい。

Research Products

• [Publications] S.Hayashi: "Testing Proofs by Examples" Lecture Notes in Computer Science. 1538. 1-3 (1998)
• [Publications] M.Banbara: "Compiling Resources in a Linear Logic Programming Language" Proc.of Workshop on Parallelism and Implementation Technology for Logic Programming Languages. 32-45 (1998)
• [Publications] M.Yasugi: "Computability problem of Gaussian function" Computability and Complexity in Analysis ed. by K-I.Ko et.al. 157-165 (1998)