@misc{oai:uec.repo.nii.ac.jp:00008699,
 author = {早川, 恵太},
 month = {2018-04-13},
 note = {2017, 一般的に，数学の定理や論理学における命題の真偽を示すには，正しく行われた証明が必要不可欠である．しかし，証明を人間の手で行う場合は，論理の飛躍や定理等の書き間違いなどのヒューマンエラーの危険性がある．この問題を解決するアプローチとして，定理証明支援系と呼ばれるシステムを利用した，計算機上で証明を記述する手法が存在する．Coqはその1つであり，過去に人の手では書ききることが困難な証明を，Coq を用いて行った研究も存在する．Coq ではユーザによって入力されるタクティクと呼ばれるコマンドによって，対話的に証明が行われる．しかし，Coq 標準のインタフェースではユーザはタクティクの羅列でしか証明を確認できず，行った証明の論理展開等の構造を確認しにくいという欠点がある．これを解決するため，本研究ではユーザにとってわかりやすい形で証明を表示しながら証明を進めることを可能とするCoqのユーザインタフェースの設計ならびに実装を行った．具体的には，関数型言語OCamlを用いてCoq内部で処理されている証明の情報を取得し，証明木という形に変換した．証明木はXML形式のデータに変換し，インタフェース側に証明木の情報を伝達できるようにした．その後，Javaで実装したインタフェースが証明木を受け取り，その情報を整理した後にわかりやすい形にして画面に表示することで，Coq 標準のインタフェースよりも証明の構造を把握しやすくした．さらに，本インタフェース上でCoqに対する操作を行えるようにすることで，本インタフェースだけでユーザの操作が完結するように実装した．また，幾つかの機能を実装することで，特にCoqや論理
学の初学者にとって証明の構造や推移がわかりやすい形で証明を扱うことができるように設計した．これらにより，証明の視認性の向上や初心者及び初学者に対する証明操作の手助けという本研究の目的に寄与することができた．},
 title = {定理証明支援系Coqにおける証明木を操作可能なインタフェースの設計および実装},
 year = {},
 yomi = {ハヤカワ, ケイタ}
}