Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 DetailsÜbersicht
  Decidability Results for Saturation-Based Model Building

Horbach, M., & Weidenbach, C. (2009). Decidability Results for Saturation-Based Model Building. In R. Schmidt (Ed.), 22nd International Conference on Automated Deduction (CADE-22) (pp. 404-420). Heidelberg: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1A4E-D Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BB85-C
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Horbach, Matthias1, Autor           
Weidenbach, Christoph1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. We extend our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting. Based on this calculus, we present several new decidability results for validity in the minimal model of a satisfiable finitely saturated clause set that in particular extend the decidability results known for ARM (Atomic Representations of term Models) and DIG (Disjunctions of Implicit Generalizations) model representations.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2009-10-232009
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521087
Anderer: Local-ID: C125716C0050FB51-960E286C41E4B7F4C12575A20036CB2F-HorbachWeidenbach2009CADE
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Montreal, Canada
Start-/Enddatum: 2009-08-02 - 2009-08-07

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: 22nd International Conference on Automated Deduction (CADE-22)
Genre der Quelle: Konferenzband
 Urheber:
Schmidt, Renate, Herausgeber
Affiliations:
-
Ort, Verlag, Ausgabe: Heidelberg : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 404 - 420 Identifikator: -

Quelle 2

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