Coq 证明脚本可视化工具 (coq-psv)
计算机科学中的逻辑
2021-01-20 v1 计算机与社会
摘要
在本工作中,我们提出一种可视化工具,能够处理 Coq 证明脚本并生成所包含证明的表格表示,输出为 或 PDF 文件。该工具旨在支持教学与评审过程,因为所有证明步骤均可被可视化。因此,无需使用 Coq 即可评审证明或将其作为教学示例。与通常将证明可视化为超文本或 markdown 文档的方法不同,所生成的文件易于打印。
引用
@article{arxiv.2101.07761,
title = {The Coq Proof Script Visualiser (coq-psv)},
author = {Mario Frank},
journal= {arXiv preprint arXiv:2101.07761},
year = {2021}
}
备注
This contribution was presented during a talk at the Coq Workshop 2020, affiliated with the IJCAR 2020