Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Theorem proving in cancellative abelian monoids

Ganzinger, Harald and Waldmann, Uwe

MPI-I-96-2-001. January 1996, 52 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We describe a refined superposition calculus for cancellative abelian monoids. They encompass not only abelian
groups, but also such ubiquitous structures as the natural numbers or multisets. Both the AC axioms and the cancellation
law are difficult for a general purpose superposition theorem prover, as they create many variants of clauses which contain sums.
Our calculus requires neither explicit inferences with the theory clauses for cancellative abelian monoids nor extended equations
or clauses. Improved ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum
in the maximal literal. Furthermore, the search space is reduced drastically by certain variable elimination techniques.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-96-2-001.psMPI-I-96-2-001.pdf398 KBytes; 443 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Ganzinger, Harald and Waldmann, Uwe},
  TITLE = {Theorem proving in cancellative abelian monoids},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-96-2-001},
  MONTH = {January},
  YEAR = {1996},
  ISSN = {0946-011X},