User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

Superposition Theorem Proving for Abelian Groups Represented as Integer Modules


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

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Stuber, J. (1996). Superposition Theorem Proving for Abelian Groups Represented as Integer Modules. In H. Ganzinger (Ed.), 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
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.