合并覆盖与 Beth 可定义性（扩展版）
计算机科学中的逻辑
2020-07-01 v3
摘要
在 ESOP 2008 上，Gulwani 与 Musuvathi 引入了一种覆盖的概念，并利用它来处理无限状态模型检验问题。受数据感知过程验证应用的推动，我们在先前的一篇论文中证明了覆盖与模型完备性（模型论中一个众所周知的主题）严格相关。本文研究在互不相交签名情形下覆盖向理论组合的转移。我们证明，对于凸理论，覆盖算法可在与转移无量词插值相同的假设（等式插值性质亦称强合并性质）下转移到理论组合中。在非凸情形下，我们通过一个反例表明，即便组合后的无量词插值确实存在，覆盖在组合理论中也可能不存在。然而，我们给出了一种也在非凸情形下适用于特殊理论组合的覆盖转移算法；这些组合（称为“驯良组合”）涉及在许多模型检验应用（特别是面向数据感知过程验证的应用）中出现的多排序理论。
引用
@article{arxiv.1911.07774,
title = {Combined Covers and Beth Definability (Extended Version)},
author = {Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin},
journal= {arXiv preprint arXiv:1911.07774},
year = {2020}
}