Datensatz

Zusammenfassung

We present a general approach for integrating certain mathematical structures
in first-order equational theorem provers. More specifically, we consider
theorem proving problems specified by sets of first-order clauses that contain
the axioms of a commutative ring with a unit element. Associative-commutative
superposition forms the deductive core of our method, while a convergent
rewrite system for commutative rings provides a starting point for more
specialized inferences tailored to the given class of formulas. We adopt ideas
from the Gr{\"o}bner basis method to show that many inferences of the
superposition calculus are redundant. This result is obtained by the judicious
application of the simplification techniques afforded by convergent rewriting
and by a process called symmetrization that embeds inferences between single
clauses and ring axioms.