Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)

Author: Waldmann U.  

Publisher: Academic Press

ISSN: 0747-7171

Source: Journal of Symbolic Computation, Vol.33, Iss.6, 2002-06, pp. : 831-861

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Cancellative superposition is a refutationally complete calculus for first-order equational theorem proving in the presence of the axioms of cancellative Abelian monoids, and, optionally, the torsion-freeness axioms. Thanks to strengthened ordering restrictions, cancellative superposition avoids some of the inefficiencies of classical AC-superposition calculi. We show how the efficiency of cancellative superposition can be further improved by using variable elimination techniques, leading to a significant reduction of the number of variable overlaps. In particular, we demonstrate that in divisible torsion-free Abelian groups, variable overlaps, AC-unification and AC-orderings can be avoided completely.