定理証明支援系Coq と連携した証明木図示ツールにおける大域的および局所的な情報把握支援機能の改善

摘要

定理の証明やソフトウェア検証の場面で，形式的に証明するために定理証明支援系Coqが広く利用される．Coq を用いた証明スクリプトは，手続き型の記述が行われるため，可読性が高いとは言い難く，証明全体を詳細に見通し確認する行為は労力を要する．我々の研究目的は，Coq を用いて証明を遂行するユーザへの情報の把握支援である．証明木全体の概要を見通す大域的な支援と証明時点のサブゴールに対して推論規則を適用するための局所的な支援の二つの視点での支援が重要である．