Incremental Instance Generation in Local Reasoning

Jacobs, Swen

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Incremental Instance Generation in Local Reasoning

MPS-Authors

/persons/resource/persons44687

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-1BEC-3

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.