Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Jacobs, Swen

dblp



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

URL of the conference:

http://www.mpi-inf.mpg.de/~sofronie/cedar08.html

URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
IIGLR.pdf