Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)

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

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AC21-A Versions-Permalink: https://hdl.handle.net/21.11116/0000-000E-38D8-0
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
https://rdcu.be/dv0xz (Verlagsversion)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

einblenden:
ausblenden:
 Urheber:
Ganzinger, Harald1, Autor           
Waldmann, Uwe1, 2, Autor                 
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121996
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519898
Anderer: Local-ID: C1256104005ECAFC-D3B31BC55873B750C12564610057884F-GanzingerWaldmann1996CADE
BibTex Citekey: Ganzinger-Waldmann_CADE96
DOI: 10.1007/3-540-61511-3_102
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 13th International Conference on Automated Deduction
Veranstaltungsort: New Brunswick, USA
Start-/Enddatum: 1996-07-30 - 1996-08-03

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated Deduction - CADE-13
  Untertitel : 13th International Conference on Automated Deduction
  Kurztitel : CADE 1996
Genre der Quelle: Konferenzband
 Urheber:
McRobbie, Michael A.1, Herausgeber
Slaney, John K.1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 388 - 402 Identifikator: ISBN: 978-3-540-61511-8

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
  Kurztitel : LNAI
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 1104 Artikelnummer: - Start- / Endseite: - Identifikator: -