Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  New Directions in Instantiation-Based Theorem Proving

Ganzinger, H., & Korovin, K. (2003). New Directions in Instantiation-Based Theorem Proving. In 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03) (pp. 55-64). Los Alamitos, USA: IEEE.

Item is

Dateien

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

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Ganzinger, Harald1, Autor           
Korovin, Konstantin1, Autor           
Kolaitis, Phokion, Herausgeber
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2004-06-172003
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 202019
Anderer: Local-ID: C1256104005ECAFC-9F899010FD50E7D7C1256D170066FF4B-GanzingerKorovin-03-lics
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: LICS 2003
Veranstaltungsort: Ottawa, Canada
Start-/Enddatum: 2003-06-22 - 2003-06-25

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03)
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Los Alamitos, USA : IEEE
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 55 - 64 Identifikator: ISBN: 0-7695-1884-2