关于理论扩展中的插值和符号消除
摘要：在本文中，我们研究了在具有附加函数符号的理论扩展中插值和符号消除的可能性，其属性通过一组子句公理化。我们分析了可以通过层次化的方式执行此类任务的情况，依赖于现有的针对$mathcal{T}\_0$中符号消除的机制。例如，如果基本理论允许量词消除，则可以实现这一点。我们分析了将这些方法扩展到基本理论不允许量词消除但具有模型补充的情况的可能性。我们通过各种示例说明了该方法。
作者：Viorica Sofronie-Stokkermans
论文ID：1702.06620
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22