English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  DetailsSummary

Released
Journal Article

Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I)

MPS-Authors
/persons/resource/persons45689

Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
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

Waldmann, U. (2002). Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I). Journal of Symbolic Computation, 33, 777-829.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2F2E-3
Abstract
We present superposition calculi in which the axioms of cancellative abelian monoids and, optionally, the torsion-freeness axiom are integrated. Cancellative abelian monoids comprise abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Our calculi require neither extended clauses nor explicit inferences with the theory axioms. Compared with AC-superposition calculi, the number of variable overlaps is significantly reduced by strong ordering restrictions.