MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Jacobs, Swendblp
Editor(s):
Baader, Franz
Ghilardi, Silvio
Hermann, Miki
Sattler, Ulrike
Sofronie-Stokkermans, Viorica
dblp
dblp
dblp
dblp
dblp
Not MPII Editor(s):
Baader, Franz
Ghilardi, Silvio
Hermann, Miki
Sattler, Ulrike
BibTeX cite key*:
Jacobs2008
Title, Booktitle
Title*:
Incremental Instance Generation in Local Reasoning
IIGLR.pdf (199.57 KB)
Booktitle*:
Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08
Event, URLs
Conference URL::
http://www.mpi-inf.mpg.de/~sofronie/cedar08.html
Downloading URL:
http://www.mpi-inf.mpg.de/~sjacobs/publications/CEDAR08.pdf
Event Address*:
Sydney, Australia
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
10 August 2008
Event End Date:
10 August 2008
Publisher
Name*:

This proceedings has no publisher!
URL:
Address*:
Sydney, Australia
Type:
Vol, No, Year, pp.
Series:
Volume:
Number:
Month:
August
Pages:
47-62
Year*:
2008
VG Wort Pages:
37
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
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.
Keywords:
Local Reasoning, SMT, Instantiation, Instance Generation, Locality
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{Jacobs2008,
AUTHOR = {Jacobs, Swen},
EDITOR = {Baader, Franz and Ghilardi, Silvio and Hermann, Miki and Sattler, Ulrike and Sofronie-Stokkermans, Viorica},
TITLE = {Incremental Instance Generation in Local Reasoning},
BOOKTITLE = {Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08},
YEAR = {2008},
PAGES = {47--62},
ADDRESS = {Sydney, Australia},
MONTH = {August},
}


Entry last modified by Swen Jacobs, 03/03/2009
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Swen Jacobs
Created
12/04/2008 12:01:53 PM
Revision
1.
0.


Editor
Swen Jacobs
Swen Jacobs


Edit Date
12/04/2008 12:03:01 PM
12/04/2008 12:01:53 PM



File Attachment Icon
IIGLR.pdf