# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Superposition Theorem Proving for Abelian Groups Represented as Integer Modules

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Stuber, J. (1996). Superposition Theorem Proving for Abelian Groups Represented as
Integer Modules. In H. Ganzinger (*Rewriting Techniques
and Applications, 7th International Conference, RTA-96* (pp. 33-47). Berlin, Germany: Springer.

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

##### Abstract

We define a superposition calculus specialized for abelian
groups represented as integer modules, and show its
refutational completeness. This allows to substantially
reduce the number of inferences compared to a standard
superposition prover which applies the axioms directly.
Specifically, equational literals are simplified, so that
only the maximal term of the sums is on the left-hand
side. Only certain minimal superpositions need to be
considered; other superpositions which a standard prover
would consider become redundant. This not only reduces
the number of inferences, but also reduces the size of the
AC-unification problems which are generated. That is,
AC-unification is not necessary at the top of a term, only
below some non-AC-symbol. Further, we consider situations
where the axioms give rise to variable overlaps and
develop techniques to avoid these explosive cases where
possible.