论文标题
吸血鬼中饱和尝试的交互式可视化
Interactive Visualization of Saturation Attempts in Vampire
论文作者
论文摘要
许多正式方法的应用都需要有关系统属性的自动推理，例如系统安全和保障。为了提高自动推理引擎的性能，例如SAT/SMT求解器和一阶定理供奉献者，有必要了解这些引擎在生产正式证书（例如逻辑证明和/或模型）方面的成功和失败尝试。由于在证明/模型搜索过程中生成的大量逻辑公式，因此这种分析具有挑战性。在本文中，我们关注基于饱和的一阶定理证明并介绍SATVIS工具，用于以一阶定理证明基于饱和的证明尝试。我们通过互动地可视化萨特维斯吸血鬼的饱和尝试，在世界领先的定理宣传吸血鬼的顶部建立了萨维斯。我们的工作结合了饱和尝试与交互式转换和搜索功能引起的衍生图的自动布局和可视化。结果，我们能够分析和调试吸血鬼的证明尝试。由于其交互式可视化，我们相信Satvis可以帮助定理中的专家和非专家，这些专家和非专家都证明了一阶证明并分析/完善一阶抛弃的失败证明尝试。
Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or models. Such an analysis is challenging due to the large number of logical formulas generated during proof/model search. In this paper we focus on saturation-based first-order theorem proving and introduce the SATVIS tool for interactively visualizing saturation-based proof attempts in first-order theorem proving. We build SATVIS on top of the world-leading theorem prover VAMPIRE, by interactively visualizing the saturation attempts of VAMPIRE in SATVIS. Our work combines the automatic layout and visualization of the derivation graph induced by the saturation attempt with interactive transformations and search functionality. As a result, we are able to analyze and debug (failed) proof attempts of VAMPIRE. Thanks to its interactive visualisation, we believe SATVIS helps both experts and non-experts in theorem proving to understand first-order proofs and analyze/refine failing proof attempts of first-order provers.
