Superposition Theorem Proving for Abelian Groups Represented as Integer Modules

Stuber, Jürgen

doi:10.1007/3-540-61464-8_41

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Superposition Theorem Proving for Abelian Groups Represented as Integer Modules

MPS-Authors

/persons/resource/persons45567

Stuber, Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

https://rdcu.be/dvCHe
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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 (Ed.), Rewriting Techniques and Applications (pp. 33-47). Berlin, Germany: Springer.

Cite as: https://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.