论文标题
理论推理的分层条款选择
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 theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms.
