de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Theorem proving in cancellative abelian monoids

MPG-Autoren
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
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

1996-2-001
(beliebiger Volltext), 11KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Ganzinger, H., & Waldmann, U.(1996). Theorem proving in cancellative abelian monoids (MPI-I-1996-2-001). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-9FF7-2
Zusammenfassung
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.