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.
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.
Related content
Superposition theorem proving for abelian groups represented as integer modules
By Stuber J.
Theoretical Computer Science, Vol. 208, Iss. 1, 1998-11 ,pp. :
Theorem proving by chain resolution
Theoretical Computer Science, Vol. 206, Iss. 1, 1998-10 ,pp. :
By Dowek Gilles Hardin Thérèse Kirchner Claude
Journal of Automated Reasoning, Vol. 31, Iss. 1, 2003-09 ,pp. :