基于SAT的子包含消解
SAT-Based Subsumption Resolution
AI总结：
针对一阶饱和定理证明器中的子包含消解问题，提出无需改动底层饱和算法的基于SAT的推理技术，在Vampire中实现后速度优于现有最优水平。
摘要：
子包含消解是一阶饱和定理证明器中一种开销大但高效的简化推理方法。我们提出了一种新的基于SAT的子包含消解推理技术，无需对底层饱和算法做根本性改动。我们在定理证明器Vampire中实现了该方法，结果显示其速度明显快于现有最优技术。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
