Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Integration of equational reasoning into instantiation-based theorem proving

Ganzinger, H., & Korovin, K. (2004). Integration of equational reasoning into instantiation-based theorem proving. In Computer science logic: 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL (pp. 71-84). Berlin: Springer.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ganzinger, Harald1, Autor           
Korovin, Konstantin1, Autor           
Marcinkowski, Jerzy1, Herausgeber           
Tarlecki, Andrzej, Herausgeber
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: In this paper we present a method for integrating equational reasoning into instantiation-based theorem proving. The method employs a satisfiability solver for ground equational clauses together with an instance generation process based on an ordered paramodulation type calculus for literals. The completeness of the procedure is proved using the the model generation technique, which allows us to justify redundancy elimination based on appropriate orderings.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-02-022004
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 231251
Anderer: Local-ID: C1256104005ECAFC-BF63DC0F8D07033EC1256F90005FF675-GanzKor:InstEq:2004
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Karpacz, Poland
Start-/Enddatum: 2004-09-20

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 71 - 84 Identifikator: ISBN: 3-540-23024-6

Quelle 2

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