MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-2001-2-001

Superposition and chaining for totally ordered divisible abelian groups

Waldmann, Uwe

April 2001, 40 pages.

.
Status: available - back from printing

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.

  • MPI-I-2001-2-001.ps
  • Attachement: MPI-I-2001-2-001.ps (477 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2001-2-001

Hide details for BibTeXBibTeX
@TECHREPORT{WaldmannMPI-I-2001-2-001,
  AUTHOR = {Waldmann, Uwe},
  TITLE = {Superposition and chaining for totally ordered divisible abelian groups},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2001-2-001},
  MONTH = {April},
  YEAR = {2001},
  ISSN = {0946-011X},
}