# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings

##### MPS-Authors

##### 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

Bachmair, L., Ganzinger, H., & Stuber, J. (1995). Combining Algebra and Universal
Algebra in First-Order Theorem Proving: The Case of Commutative Rings. In E. Astesiano, G. Reggio, & A. Tarlecki (*Recent Trends in Data Type Specification. 10th Workshop on Specification
of Abstract Data Types Joint with the 5th COMPASS Workshop* (pp. 1-29). Berlin, Germany: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-ACF0-7

##### Abstract

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.