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.
翻译:众所周知,由于这些轴心的宏大性质,以关联性与共通性(AC)的存在为理由,具有挑战性。对ACxioms的专门处理主要得到基于Knuth-Bendix完成的单位平等证明者的支持。这些证明中处理AC的主要成份是适合AC的地面共通性标准。在本文件中,我们将AC的共通性从单位等同和Knuth-Bendix完成到超位微积分和完全一阶逻辑的方面扩展为共同性。我们的方法基于Bachmair-Ganzinger模型构建的扩展和涵盖地面共通性的新的冗余标准。我们方法的副产品是我们称之为包含分解的演示适用性新标准。这一标准在任何超位词体验证中都是有用的,独立于AC理论,我们证明它能够比标准在更多的情况下进行退缩。