叠加演算中的AC化简与闭包冗余
AC Simplifications and Closure Redundancies in the Superposition Calculus
摘要：
结合性和交换性（AC）的存在下的推理是众所周知的挑战，由于这些公理的多产性。AC公理的专业化处理主要是由基于Knuth-Benzynn完备的单位等式证明器支持的。在这些验证器中处理AC的主要成分是适用于AC的地面可连接性标准。本文将AC可连接性从单位等式和Knuth-Beneficiary完备化推广到叠加演算和全一阶逻辑。我们的方法是基于扩展的Bachmair-Ganzinger模型建设和一个新的冗余标准，其中包括地面可连接性。我们的方法的一个副产品是一个新的标准，适用性的解调，我们称之为解调器解调。这个标准是有用的，在任何叠加定理证明，独立的AC理论，我们证明，它使解调在更多的情况下，相比标准标准。
英文摘要：
Reasoning in the presence of associativity and commutativity (AC) is well known to be challenging due to prolific nature of these axioms. Specialised treatment of AC axioms is mainly supported by provers for unit equality which are based on Knuth-Bendix completion. The main ingredient for dealing with AC in these provers are ground joinability criteria adapted for AC. In this paper we extend AC joinability from the context of unit equalities and Knuth-Bendix completion to the superposition calculus and full first-order logic. Our approach is based on an extension of the Bachmair-Ganzinger model construction and a new redundancy criterion which covers ground joinability. A by-product of our approach is a new criterion for applicability of demodulation which we call encompassment demodulation. This criterion is useful in any superposition theorem prover, independently of AC theories, and we demonstrate that it enables demodulation in many more cases, compared to the standard criterion.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
