Interpolation in local theory extensions

TL;DR

This paper explores hierarchical interpolation in local theory extensions, enabling efficient computation of interpolants for verification and reasoning by leveraging base theory procedures.

Contribution

It introduces a method for hierarchical interpolation in local theory extensions, with practical examples and applications in verification and modular reasoning.

Findings

Interpolants can be computed hierarchically in certain local theory extensions.

The approach uses a prover and a black-box interpolant generator for the base theory.

Applications include verification, knowledge representation, and modular reasoning.

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.