In Michael A. McRobbie and John K. Slaney, editors, Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, LNAI 1104, pages 388-402, New Brunswick, NJ, USA, July 30-August 3, 1996. Springer-Verlag. [Postscript file, 58 kB]
Full version: Technical Report MPI-I-96-2-001, Max-Planck-Institut für Informatik, Saarbrücken, January 1996. [Postscript file, 145 kB]
Abstract: Cancellative abelian monoids encompass abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Both the AC axioms and the cancellation law are difficult for a general purpose theorem prover, as they create many variants of clauses which contain sums. We describe a refined superposition calculus for cancellative abelian monoids which requires neither explicit inferences with the theory clauses nor extended equations or clauses. Strong ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum in the maximal literal. Besides, the search space is reduced drastically by variable elimination techniques.