Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Conference Paper

Interpolation in local theory extensions


Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

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.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-24CD-F
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.