礼貌已不够（以及理论组合的其他局限）
计算机科学中的逻辑
2025-05-22 v2 逻辑
摘要
在满足基理论的 Nelson-Oppen 组合方法中，组合后的理论必须满足稳定无限性；在温和组合中，需要一个理论满足温和条件，另一个理论需满足类似但较弱的属性；在闪亮组合中，仅需一个理论满足闪亮条件（即光滑、具有可计算最小模型函数且具有有限模型属性）；而在礼貌组合中，仅需一个理论满足强礼貌条件（即光滑且强有限可 Witness）。对于每种组合方法，我们证明只要移除其中的任何假设，就不存在一种通用方法来组合满足剩余假设的任意两组理论。我们还证明了一些削弱温和和闪亮组合假设的新理论组合结果。
关键词
引用
@article{arxiv.2505.04870,
title = {Being polite is not enough (and other limits of theory combination)},
author = {Guilherme V. Toledo and Benjamin Przybocki and Yoni Zohar},
journal= {arXiv preprint arXiv:2505.04870},
year = {2025}
}