Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Incremental Instance Generation in Local Reasoning

Jacobs, S. (2008). Incremental Instance Generation in Local Reasoning. In F. Baader, S. Ghilardi, M. Hermann, U. Sattler, & V. Sofronie-Stokkermans (Eds.), Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08 (pp. 47-62). Sydney, Australia: CEDAR.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Jacobs, Swen1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate this set incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2009-03-252008
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 428275
URI: http://www.mpi-inf.mpg.de/~sjacobs/publications/CEDAR08.pdf
Anderer: Local-ID: C125756E0038A185-2CEFBAF5CDB1BD02C1257515003C9921-Jacobs2008
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Sydney, Australia
Start-/Enddatum: 2008-08-10 - 2008-08-10

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08
Genre der Quelle: Konferenzband
 Urheber:
Baader, Franz, Herausgeber           
Ghilardi, Silvio, Herausgeber
Hermann, Miki, Herausgeber
Sattler, Ulrike, Herausgeber
Sofronie-Stokkermans, Viorica1, Herausgeber           
Affiliations:
1 Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545            
Ort, Verlag, Ausgabe: Sydney, Australia : CEDAR
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 47 - 62 Identifikator: -