Interpolation in Local Theory Extensions

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.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Viorica Sofronie-Stokkermans
• Keywords: Base Theory, CADE 2006, Hierarchical Manner, Local Extensions, Logical Reasoning