6J-03
定理証明支援系Coqと連携した証明木表示機能の設計と実装
○木村麻衣（広島市大），田中雄太（関電システムソリューションズ），川端英之，弘中哲夫（広島市大）
定理証明支援系Coqを用いた証明スクリプトは手続き的な記述であるため,可読性が高いとは言い難い.対話的な証明手続きの各時点での状況把握や完了した証明の俯瞰の補助には,証明の流れをグラフィカルに表示する機能が有用だと考えられる.Coqは対話的な証明の過程をグラフ構造で描画するツールProoftreeと連携できるが,適用した推論規則の流れのみを簡易的なグラフ構造で描画するため,証明の詳細な把握には向いていない. 本研究では,描画する情報量を適切に抑え,自然演繹で用いられる読みやすいスタイルで証明を提示できる機能を設計した.本発表では,Prooftreeの改造による本機能の設計と実装について報告する.
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会