Interpolation in local theory extensions

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.

31 pages, 1 figure

Cited by in corpus (10)

• Quantifier-Free Interpolation of a Theory of Arrays
• On Interpolation and Symbol Elimination in Theory Extensions
• On First-Order Model-Based Reasoning
• NIL: Learning Nonlinear Interpolants
• Nonlinear Craig Interpolant Generation
• On combinations of local theory extensions
• Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
• Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)
• Locality and applications to subsumption testing and interpolation in $\mathcal{E}\mathcal{L}$ and some of its extensions
• System Description: H-PILoT (Version 1.9)