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. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Waldmann, U. (2001). Superposition and chaining for totally ordered divisible abelian groups. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 226–241). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_17
Mendeley helps you to discover research relevant for your work.