一阶定理证明中的包容解调
Subsumption Demodulation in First-Order Theorem Proving
摘要：
受一阶定理证明在软件分析中应用的启发，我们引入了一个新的推理规则，称为包容解调，以提高对基于叠加的定理证明中条件等式推理的支持。我们发现，包容解调是一个简化的规则，不需要根本的变化，基本的叠加演算。我们在定理证明器Vampire中实现了包容解调，通过扩展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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
