ProofTool 中的高级证明查看
计算机科学中的逻辑
2014-10-31 v1 人机交互
摘要
相继式演算广泛用于形式化证明。然而，由于数据的激增，理解甚至简单数学论证的证明很快就变得不可能。图形用户界面有助于解决这一问题，但由于它们通常采用 Gentzen 的原始记号，一些问题依然存在。在本文中，我们引入了一系列我们认为对分析证明至关重要的证明可视化标准。随后，我们根据这些标准评估了树可视化的最新进展，并提出 Sunburst Tree 布局作为传统树结构的补充。该布局将推理构建为围绕根推理的同心圆弧，使用户能够专注于证明的结构内容。最后，我们描述了其在 ProofTool 中的集成，并解释了它如何与 Gentzen 布局交互。
引用
@article{arxiv.1410.8218,
title = {Advanced Proof Viewing in ProofTool},
author = {Tomer Libal and Martin Riener and Mikheil Rukhaia},
journal= {arXiv preprint arXiv:1410.8218},
year = {2014}
}
备注
In Proceedings UITP 2014, arXiv:1410.7850