English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  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

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1BEC-3 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BBD2-D
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Jacobs, Swen1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2009-03-252008
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 428275
URI: http://www.mpi-inf.mpg.de/~sjacobs/publications/CEDAR08.pdf
Other: Local-ID: C125756E0038A185-2CEFBAF5CDB1BD02C1257515003C9921-Jacobs2008
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Sydney, Australia
Start-/End Date: 2008-08-10 - 2008-08-10

Legal Case

show

Project information

show

Source 1

show
hide
Title: Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08
Source Genre: Proceedings
 Creator(s):
Baader, Franz, Editor           
Ghilardi, Silvio, Editor
Hermann, Miki, Editor
Sattler, Ulrike, Editor
Sofronie-Stokkermans, Viorica1, Editor           
Affiliations:
1 Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545            
Publ. Info: Sydney, Australia : CEDAR
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 47 - 62 Identifier: -