论理论扩展中的符号消去与一致插值
计算机科学中的逻辑
2025-06-03 v1
摘要
我们定义了一般一致插值的概念，推广了覆盖和一致插值的概念，并确定了可以使用符号消去来计算一般一致插值的情形。我们研究了所提方法的局限性，并确定了一类理论扩展，对于这些扩展，一般一致插值的计算可以归约为符号消去，随后在允许一致无量词插值的理论的未解释函数符号扩展中进行无量词一致插值的计算。
引用
@article{arxiv.2506.01664,
title = {On Symbol Elimination and Uniform Interpolation in Theory Extensions},
author = {Viorica Sofronie-Stokkermans},
journal= {arXiv preprint arXiv:2506.01664},
year = {2025}
}
备注
33 pages