定理証明支援系のGUIにおける証明木表示機能の拡張

• Item type: Symposium_02(1)
• 公開日: 2016-01-08
• タイトル: 定理証明支援系のGUIにおける証明木表示機能の拡張
• タイトル / 言語: en
• タイトル: Extension of a Proof Assistant's GUI for Displaying Traditional Proof Trees
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 定理証明支援系，証明木，Coq，ProofGeneral，GUI
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 広島市立大学大学院情報科学研究科
• 著者所属: 広島市立大学大学院情報科学研究科
• 著者所属: 広島市立大学大学院情報科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Sciences, Hiroshima City University
• 著者名: 田中, 雄太; 川端, 英之; 北村, 俊明
• 著者名(英): Yuta, Tanaka; Hideyuki, Kawabata; Toshiaki, Kitamura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ソフトウェアの検証や数学的な定理証明のために，定理証明支援系が利用されている．しかし，既存の定理証明系及びそのユーザインタフェースには，初学者には使い難い点がある．例えば，定理証明支援系CoqなどのインタフェースであるProofGeneralの備える証明木可視化ツールProoftreeは，極度に簡略化された証明木しか表示する機能を持たない．本研究では，Prooftreeに注目し，定理証明支援系の初学者や，数理論理学で一般に用いられる証明木に慣れているユーザを対象に，より分かり易い木を表示する機能や，証明の進行を制御する機能を導入する．これにより，ProofGeneralに慣れていないユーザや，標準証明木に慣れているユーザに対し，より効果的に証明の支援を行えると期待できる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Proof assistants (or, interactive theorem provers) have been used for verifying software and/or proving theorems. However, existing theorem provers and their UIs are not very easy for novices to use. For example, Prooftree, a proof tree viewer of ProofGeneral, only displays extremely simplified proof trees. We are planning to extend Prooftree's UI such that the user can easily grasp details of proofs looking at ordinary textbook-style trees, and in addition, interaction between the user and ProofGeneral can be carried out through the proof tree viewer. The extension is expected to offer easier ways to access to proof assistants.
• 書誌情報: 第57回プログラミング･シンポジウム予稿集; 巻 2016, p. 67-72, 発行日 2016-01-08
• 出版者 / 言語: ja
• 出版者: 情報処理学会