On Interpolation and Symbol Elimination in Theory Extensions

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.

Cited by in corpus (4)

• Quantifier Elimination for Database Driven Verification
• Symbol Elimination for Parametric Second-Order Entailment Problems (with Applications to Problems in Wireless Network Theory)
• Combined Covers and Beth Definability (Extended Version)
• Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)