Vampire中饱和尝试的交互式可视化
计算机科学中的逻辑
2020-01-14 v1
摘要
形式化方法的许多应用需要对系统属性（如系统安全性与安全性）进行自动推理。为提升自动推理引擎（如SAT/SMT求解器和一阶定理证明器）的性能，有必要理解这些引擎在生成形式化证书（如逻辑证明和/或模型）过程中的成功与失败尝试。由于证明/模型搜索期间生成的大量逻辑公式，此类分析具有挑战性。本文关注基于饱和的一阶定理证明，并介绍了SATVIS工具，用于交互式可视化一阶定理证明中基于饱和的证明尝试。我们在世界领先定理证明器VAMPIRE之上构建SATVIS，通过在SATVIS中交互式可视化VAMPIRE的饱和尝试。我们的工作将饱和尝试所诱导的推导图的自动布局与可视化，同交互式变换和搜索功能相结合。因此，我们能够分析和调试VAMPIRE的（失败）证明尝试。得益于其交互式可视化，我们相信SATVIS有助于定理证明领域的专家与非专家理解一阶证明并分析/改进一阶证明器的失败证明尝试。
引用
@article{arxiv.2001.04100,
title = {Interactive Visualization of Saturation Attempts in Vampire},
author = {Bernhard Gleiss and Laura Kovacs and Lena Schnedlitz},
journal= {arXiv preprint arXiv:2001.04100},
year = {2020}
}