一种用于证明策略的图形语言
计算机科学中的逻辑
2014-06-13 v2
摘要
复杂的自动化证明策略通常难以提取、可视化、修改和调试。传统的策略语言通常基于基于栈的目标传播，使得编写的证明容易掩盖策略之间的目标流，并且对输入、证明结构或策略本身的微小变化很脆弱。在这里，我们通过引入一种名为PSGraph的图形语言来编写证明策略来解决这个问题。策略通过将策略集合“连接在一起”以视觉方式构建，并通过图重写传播目标节点来评估。策略节点可以有多个输出线，并使用基于目标类型（描述目标特征的谓词）的过滤过程来决定将新生成的子目标发送到何处。除了使目标信息流显式化外，该图形语言还可以使用视觉习语（如分支、合并和反馈循环）来发挥许多策略组合子的作用。我们认为，这种语言能够开发更健壮的证明策略，并提供了几个示例，以及在Isabelle中的原型实现。
引用
@article{arxiv.1302.6890,
title = {A Graphical Language for Proof Strategies},
author = {Gudmund Grov and Aleks Kissinger and Yuhui Lin},
journal= {arXiv preprint arXiv:1302.6890},
year = {2014}
}