具有传递守卫及相关变体的双变量守卫片段的有限可满足性
计算机科学中的逻辑
2024-04-08 v3
摘要
我们考虑双变量守卫片段 GF2 的扩展，其中仅出现在守卫中的区别二元谓词被要求以特殊方式解释（作为传递关系、等价关系、预序或偏序）。我们证明，唯一保留有限（指数）模型性质的片段是不带等词的等价守卫 GF2。对于其余片段，我们证明最小有限模型的大小至多是双指数的。为获得该结果，我们发明了一种构建有限模型的策略，该模型由放置在圆柱面上的若干多维网格构成。该构造给出了这些片段的有限可满足性问题复杂度的 2NExpTime 上界。我们改进了边界并为所有考虑的片段获得了最优边界，特别是等价守卫 GF2 为 NExpTime，传递守卫 GF2 为 2ExpTime。为获得我们的结果，我们本质上使用了整数规划的一些结果。
引用
@article{arxiv.1611.03267,
title = {Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants},
author = {Emanuel Kieronski and Lidia Tendera},
journal= {arXiv preprint arXiv:1611.03267},
year = {2024}
}
备注
Accepted for ACM TOCL