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: Goto entry point

 Author, Editor
 Author(s): Sofronie-Stokkermans, Viorica dblp
 Editor(s): Furbach, Ulrich Shankar, Natarajan dblp dblp Not MPII Editor(s): Furbach, Ulrich Shankar, Natarajan
 BibTeX cite key*: Sofronie-ijcar-06

 Title, Booktitle
 Title*: Interpolation in local theory extensions sofronie-ijcar-06.pdf (192.37 KB) Booktitle*: Proceedings of IJCAR 2006

 Event, URLs
 URL of the conference: http://ijcar06.uni-koblenz.de/ URL for downloading the paper: Event Address*: Seattle, USA Language: English Event Date* (no longer used): Organization: Event Start Date: 17 August 2006 Event End Date: 21 August 2006

 Publisher
 Name*: Springer URL: http://www.springer-ny.com/ Address*: New York Type:

 Vol, No, Year, pp.
 Series: Lecture Notes in Artificial Intelligence
 Volume: 4130 Number: Month: Pages: 235-250 Year*: 2006 VG Wort Pages: 25 ISBN/ISSN: Sequence Number: DOI:

 (LaTeX) 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. Download Access Level: Public

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort, CCL bibliography

BibTeX Entry:

@INPROCEEDINGS{Sofronie-ijcar-06,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Furbach, Ulrich and Shankar, Natarajan},
TITLE = {Interpolation in local theory extensions},
BOOKTITLE = {Proceedings of IJCAR 2006},
PUBLISHER = {Springer},
YEAR = {2006},
VOLUME = {4130},
PAGES = {235--250},
SERIES = {Lecture Notes in Artificial Intelligence},