Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Superposition and chaining for totally ordered divisible abelian groups

Waldmann, Uwe

MPI-I-2001-2-001. April 2001, 40 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2001-2-001.ps477 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  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},