Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

Incremental Instance Generation in Local Reasoning

MPG-Autoren
/persons/resource/persons44687

Jacobs,  Swen
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-1BEC-3
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.