On Interpolation and Symbol Elimination in Theory Extensions

TL;DR

This paper explores methods for interpolation and symbol elimination in theory extensions, especially focusing on hierarchical approaches and the role of quantifier elimination or model completion in the base theory.

Contribution

It introduces a framework for performing interpolation and symbol elimination in theory extensions using hierarchical methods, even when the base theory lacks quantifier elimination.

Findings

Hierarchical methods enable interpolation in certain theory extensions.

Quantifier elimination in the base theory facilitates symbol elimination.

Extensions via model completion can support these methods when quantifier elimination is absent.

Abstract

In this paper we study possibilities of interpolation and symbol elimination in extensions of a theory $\mathcal{T}_0$ with additional function symbols whose properties are axiomatised using a set of clauses. We analyze situations in which we can perform such tasks in a hierarchical way, relying on existing mechanisms for symbol elimination in $\mathcal{T}_0$. This is for instance possible if the base theory allows quantifier elimination. We analyze possibilities of extending such methods to situations in which the base theory does not allow quantifier elimination but has a model completion which does. We illustrate the method on various examples.