一句话：研究理论扩展中插值与符号消去的层次化方法，并推广至基理论仅有可量词消去模型完备的情形。
本文研究在理论 T0 通过一组子句加入额外函数符号后形成的扩展中，如何进行插值与符号消去。作者提出层次化策略：尽量复用基理论 T0 中已有的符号消去机制，而不必在扩展理论中从头处理。该方法在基理论支持量词消去时自然可行；进一步地，论文分析当基理论本身不支持量词消去、但存在可进行量词消去的模型完备时，如何把这类方法推广到扩展理论。最后通过若干例子展示方法的适用范围与处理方式。
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.
@article{paperbot375,
title = {On Interpolation and Symbol Elimination in Theory Extensions},
author = {Viorica Sofronie-Stokkermans},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:23)2018}
}