三守卫片段及相关逻辑的有穷模型理论
计算机科学中的逻辑
2021-01-26 v2 人工智能
计算复杂性
逻辑
摘要
三守卫片段（TGF）是一阶逻辑中最具表达力的可判定片段之一，它在不含等号的情况下同时包含了其双变量片段和守卫片段。我们证明了 TGF 具有有穷模型性质（给出了模型大小的紧双指数界），因此有穷可满足性与已知为 N2ExpTime-完全的可满足性相一致。利用类似的构造，我们还确立了带传递守卫的无常数（三）守卫片段的有穷可满足性的 2ExpTime-完全性。
引用
@article{arxiv.2101.08377,
title = {Finite Model Theory of the Triguarded Fragment and Related Logics},
author = {Emanuel Kieroński and Sebastian Rudolph},
journal= {arXiv preprint arXiv:2101.08377},
year = {2021}
}