非表示:
キーワード:
-
要旨:
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.
