Superposition and Chaining for Totally Ordered Divisible Abelian Groups
Uwe Waldmann
We present a first-order theorem proving calculus for totally ordered
divisible abelian groups (such as the rational numbers with + and >)
that is refutationally complete without requiring inferences with
the theory axioms or variable overlaps.
Christoph Benzmüller,
chris@ags.uni-sb.de
Last modified: Wed Sep 13 19:32:07 MEST 2000