Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Superposition Theorem Proving for Abelian Groups Represented as Integer Modules

Stuber, J. (1996). Superposition Theorem Proving for Abelian Groups Represented as Integer Modules. In H. Ganzinger (Ed.), Rewriting Techniques and Applications (pp. 33-47). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AC19-D Versions-Permalink: https://hdl.handle.net/21.11116/0000-000E-2BB0-B
Genre: Konferenzbeitrag

Externe Referenzen

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

Urheber

einblenden:
ausblenden:
 Urheber:
Stuber, Jürgen1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We define a superposition calculus specialized for abelian
groups represented as integer modules, and show its
refutational completeness. This allows to substantially
reduce the number of inferences compared to a standard
superposition prover which applies the axioms directly.
Specifically, equational literals are simplified, so that
only the maximal term of the sums is on the left-hand
side. Only certain minimal superpositions need to be
considered; other superpositions which a standard prover
would consider become redundant. This not only reduces
the number of inferences, but also reduces the size of the
AC-unification problems which are generated. That is,
AC-unification is not necessary at the top of a term, only
below some non-AC-symbol. Further, we consider situations
where the axioms give rise to variable overlaps and
develop techniques to avoid these explosive cases where
possible.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121996
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519637
Anderer: Local-ID: C1256104005ECAFC-F2E9A6E2058B3DC3C1256458004F99D3-StuberRTA96
BibTex Citekey: Stuber_RTA96
DOI: 10.1007/3-540-61464-8_41
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 7th International Conference on Rewriting Techniques and Applications
Veranstaltungsort: New Brunswick, NJ, USA
Start-/Enddatum: 1996-07-27 - 1996-07-30

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Rewriting Techniques and Applications
  Untertitel : 7th International Conference, RTA-96
  Kurztitel : RTA 1996
Genre der Quelle: Konferenzband
 Urheber:
Ganzinger, Harald1, Herausgeber           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 33 - 47 Identifikator: ISBN: 978-3-540-61464-7

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 1103 Artikelnummer: - Start- / Endseite: - Identifikator: -