图形化理解与维护证明策略，或我们如何认识到一幅图胜过 10K LoC

在交互式定理证明器中，使用函数语言将证明策略实现为证明策略（proof tactics），通常能提供简短、简洁且优雅的实现。尽管优雅，高阶特性和组合子语言的使用常导致对策略的一种非常过程化的视角，这可能与其背后的高层思想显著偏离。这会使策略难以理解，从而专家和非专家都难以调试和维护：为了分析整体策略中的失败，人们常常不得不手动拆解底层策略的复杂组合。在一个工业技术转移项目中，我们一直致力于将一个非常庞大且复杂的证明策略移植到 PSGraph（一种用于表示证明策略的图形语言，由 Tinker 工具支持）中。这项工作的目标是提高策略的可理解性和可维护性。受此初步成功的启发，我们在此通过附加的开发和调试特性扩展了 PSGraph。通过对若干现有策略的重新实现和重构，我们展示了 PSGraph 相较于典型的线性（基于项的）策略语言在调试、可读性和维护方面的优势。为了为他人提供指导，我们给出了两种方法的用户体验的相当详细的比较。本文由一个网页支持，该网页提供关于实现的进一步细节以及示例的交互式插图。