In Rajeev Goré, Alexander Leitsch, Tobias Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, LNAI 2083, pages 226-241, Siena, Italy, June 18-22, 2001. Springer-Verlag.
Corrected version of the proceedings article: [Postscript file, 88 kB]
Full version: Technical Report MPI-I-2001-2-001, Max-Planck-Institut für Informatik, Saarbrücken, April 2001. [Postscript file, 185 kB]
Abstract: We present a calculus for first-order theorem proving in the presence of the axioms of totally ordered divisible abelian groups. The calculus extends previous superposition or chaining calculi for divisible torsion-free abelian groups and dense total orderings without endpoints. As its predecessors, it is refutationally complete and requires neither explicit inferences with the theory axioms nor variable overlaps. It offers thus an efficient way of treating equalities and inequalities between additive terms over, e. g., the rational numbers within a first-order theorem prover.