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

lmcs:3157 - Logical Methods in Computer Science, September 24, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:23)2018
On Interpolation and Symbol Elimination in Theory ExtensionsArticle

Authors: Viorica Sofronie-Stokkermans

    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
    Accepted on: August 9, 2018
    Submitted on: February 23, 2017
    Keywords: Computer Science - Logic in Computer Science

    12 Documents citing this article

    Consultation statistics

    This page has been seen 1661 times.
    This article's PDF has been downloaded 478 times.