Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover Vampire, and show that it is noticeably faster than the state of the art.

翻译：包含消解是一阶饱和定理证明器中代价高昂但高效的简化推理方法。本文提出一种基于可满足性问题的新推理技术，用于实现包含消解，且无需对底层饱和算法进行根本性修改。我们在定理证明器Vampire中实现了该工作，实验表明该方法的运行速度显著优于现有技术。