# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Interpolation in local theory extensions

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

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

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-24CD-F

##### 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.