English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 DetailsSummary
  Interpolation in local theory extensions

Sofronie-Stokkermans, V. (2006). Interpolation in local theory extensions. In U. Furbach, & N. Shankar (Eds.), Proceedings of IJCAR 2006 (pp. 235-250). New York: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24CD-F Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24CF-B
Genre: Conference Paper

Files

show Files
hide Files
:
sofronie-ijcar-06.pdf (Any fulltext), 193KB
 
File Permalink:
-
Name:
sofronie-ijcar-06.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Sofronie-Stokkermans, Viorica1, 2, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory ${\cal T}_0$. In such extensions efficient hierarchical reasoning -- in which a prover for the base theory is used as a black box -- is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in ${\cal T}_0$ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.

Details

show
hide
Language(s): eng - English
 Dates: 2007-03-122006
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 521705
Other: Local-ID: C125716C0050FB51-CBB53CEA861FCCE0C125729C0035814B-Sofronie-ijcar-06
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Seattle, USA
Start-/End Date: 2006-08-17 - 2006-08-21

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of IJCAR 2006
Source Genre: Proceedings
 Creator(s):
Furbach, Ulrich, Editor
Shankar, Natarajan, Editor
Affiliations:
-
Publ. Info: New York : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 235 - 250 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 4130 Sequence Number: - Start / End Page: - Identifier: -