Sofronie-Stokkermans, Viorica - On Interpolation and Symbol Elimination in Theory Extensions

lmcs:3157 - Logical Methods in Computer Science, September 24, 2018, Volume 14, Issue 3 -
On Interpolation and Symbol Elimination in Theory Extensions

Authors: Sofronie-Stokkermans, Viorica

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.

Volume: Volume 14, Issue 3
Published on: September 24, 2018
Submitted on: February 23, 2017
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 276 times.
This article's PDF has been downloaded 232 times.