Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 DetailsÜbersicht
  Superposition modulo a Shostak Theory

Ganzinger, H., Hillenbrand, T., & Waldmann, U. (2003). Superposition modulo a Shostak Theory. In Automated Deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 182-196). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2E43-A Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2E46-4
Genre: Konferenzbeitrag

Dateien

einblenden: Dateien
ausblenden: Dateien
:
_03CADE.2.ps (beliebiger Volltext), 212KB
 
Datei-Permalink:
-
Name:
_03CADE.2.ps
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/postscript
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ganzinger, Harald1, Autor           
Hillenbrand, Thomas1, 2, 3, Autor           
Waldmann, Uwe1, 3, Autor           
Baader, Franz1, Herausgeber           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              
3Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We investigate superposition modulo a Shostak theory $T$ in order to facilitate reasoning in the amalgamation of $T$ and a free theory~$F$. % Free operators occur naturally e.\,g.\ in program verification problems when abstracting over subroutines. If their behaviour in addition can be specified axiomatically, much more of the program semantics can be captured. % Combining the Shostak-style components for deciding the clausal validity problem with the ordering and saturation techniques developed for equational reasoning, we derive a refutationally complete calculus on mixed ground clauses which result for example from CNF transforming arbitrary universally quantified formulae. % The calculus works modulo a Shostak theory in the sense that it operates on canonizer normalforms. For the Shostak solvers that we study, coherence comes for free: no coherence pairs need to be considered.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2004-06-172003
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 201853
Anderer: Local-ID: C1256104005ECAFC-4489C55BD13D7669C1256CFE005A7257-GanzingerHillenbrandWaldmann2003
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: CADE 2003
Veranstaltungsort: Miami, Florida
Start-/Enddatum: 2003-07-28 - 2003-08-02

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 182 - 196 Identifikator: ISBN: 3-540-40559-3

Quelle 2

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