论文标题
一阶定理中的补充解调证明
Subsumption Demodulation in First-Order Theorem Proving
论文作者
论文摘要
由一阶定理对软件分析证明的应用，我们介绍了一种新的推论规则，称为补充解调，以提高对基于叠加的定理中有条件平等的推理的支持。我们表明，补充解调是一个简化的规则，不需要对基本叠加的结石进行根本性更改。我们通过使用新的子句索引扩展了吸血鬼并调整其多文字匹配组件，从而在定理私人Vampire中实现了补充解调。我们使用TPTP和SMT-LIB存储库的实验表明，吸血鬼中的补充解调可以解决许多新问题，这些新问题迄今无法通过最先进的推理者解决。
Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus. We implemented subsumption demodulation in the theorem prover Vampire, by extending Vampire with a new clause index and adapting its multi-literal matching component. Our experiments, using the TPTP and SMT-LIB repositories, show that subsumption demodulation in Vampire can solve many new problems that could so far not be solved by state-of-the-art reasoners.
