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

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)

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

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45689

Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;
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

Ganzinger, H., & Waldmann, U. (1996). Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). In M. A. McRobbie, & J. K. Slaney (Eds.), Proceedings of the 13th International Conference on Automated Deduction (CADE-13) (pp. 388-402). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AC21-A
Abstract
Cancellative abelian monoids encompass 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 theorem prover, as they create many variants of clauses which contain sums. We describe a refined superposition calculus for cancellative abelian monoids which requires neither explicit inferences with the theory clauses nor extended equations or clauses. Strong ordering constraints allow us to restrict to inferences that involve the maximal term of the maximal sum in the maximal literal. Besides, the search space is reduced drastically by variable elimination techniques.