de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Superposition Theorem Proving for Abelian Groups Represented as Integer Modules

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45567

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

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

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