de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract)

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45689

Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Waldmann, U. (2001). Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract). In R. Goré, A. Leitsch, & T. Nipkow (Eds.), Automated reasoning: First International Joint Conference, IJCAR 2001 (pp. 226-241). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-3249-2
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.