Interactive Visualization of Saturation Attempts in Vampire

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)

This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.

基于SAT的子包含消解

SAT-Based Subsumption Resolution

针对一阶饱和定理证明器中的子包含消解问题，提出无需改动底层饱和算法的基于SAT的推理技术，在Vampire中实现后速度优于现有最优水平。

饱和中的程序综合

Program Synthesis in Saturation

本文提出利用基于饱和的一阶定理证明同时验证规约并综合无递归程序，扩展叠加演算并在 Vampire 中实现。

重写与归纳推理

Rewriting and Inductive Reasoning

针对传统重写在归纳推理中遗漏关键后承的问题，本文扩展 superposition 演算以在饱和中自动生成充分后承，并在 Vampire 上验证其单元等式归纳推理性能显著提升。

在饱和法中融入归纳

Getting Saturated with Induction

本文综述将归纳推理直接集成到基于饱和的一阶定理证明框架 Vampire 中的推理规则与启发式策略，并通过实验验证其实际效果。

Layered Clause Selection for Theory Reasoning

Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristical measure of the amount of …