Interpolation in local theory extensions
Logic in Computer Science
2015-07-01 v2 Software Engineering
Abstract
In this paper we study interpolation in local extensions of a base theory. 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 the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.
Cite
@article{arxiv.0806.4553,
title = {Interpolation in local theory extensions},
author = {Viorica Sofronie-Stokkermans},
journal= {arXiv preprint arXiv:0806.4553},
year = {2015}
}
Comments
31 pages, 1 figure