WEKO3
アイテム
定理証明支援系Coqと連携した証明木図示ツールにおける大域的および局所的な情報把握支援機能の改善
https://ipsj.ixsq.nii.ac.jp/records/205044
https://ipsj.ixsq.nii.ac.jp/records/2050447137ce1d-9e41-4a2b-9bcb-f7651c9fe171
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-Z82-4K-01.pdf (542.3 kB)
|
Copyright (c) 2020 by the Information Processing Society of Japan
|
| Item type | National Convention(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2020-02-20 | |||||||||||
| タイトル | ||||||||||||
| タイトル | 定理証明支援系Coqと連携した証明木図示ツールにおける大域的および局所的な情報把握支援機能の改善 | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | ソフトウェア科学・工学 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||
| 資源タイプ | conference paper | |||||||||||
| 著者所属 | ||||||||||||
| 広島市大 | ||||||||||||
| 著者所属 | ||||||||||||
| 広島市大 | ||||||||||||
| 著者所属 | ||||||||||||
| 広島市大 | ||||||||||||
| 著者名 |
古谷, 夢都
× 古谷, 夢都
× 川端, 英之
× 弘中, 哲夫
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 定理証明支援系Coqを用いた証明スクリプトは，手続き型の記述が成されるので可読性が高いとは言い難く，証明の全体構造の把握は容易とは限らない．証明の可読性向上には図示ツールが有効であると考えられる．ProofGeneralと連携した証明木描画ツールを拡張したTrafは，証明の全体構造の俯瞰的な把握に適した情報量の証明木を提示する．我々は．大域的及び局所的な観点からTrafの改良を試みている．本発表では，大きく広がりがちな証明木をコンパクトに表示するための工夫に加え，局所的に生成されるラベルの有効範囲の明示により証明ステップの詳細を把握しやすくしたGUIの設計と実装について報告する． | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AN00349328 | |||||||||||
| 書誌情報 |
第82回全国大会講演論文集 巻 2020, 号 1, p. 173-174, 発行日 2020-02-20 |
|||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
