paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Finite Model Theory of the Triguarded Fragment and Related Logics

三守卫片段及相关逻辑的有限模型论
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10 · 该论文研究三守卫片段及相关逻辑的有限模型性质与有限可满足性复杂度，属于纯逻辑/有限模型论结果，与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接关联。仅对形式化验证中可判定逻辑的理论基础有非常间接的参考价值。引用 1 inbox
Emanuel Kieronski, Sebastian Rudolph
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明三守卫片段具有有限模型性质，并确定其及相关带传递守卫片段的有限可满足性复杂度。

本文研究一阶逻辑中表达能力很强的可判定片段——三守卫片段（TGF）的有限模型论。TGF 可包含无等词的双变量片段和守卫片段。作者证明 TGF 具有有限模型性质，并给出模型大小的紧致双指数上界；由此，TGF 的有限可满足性与可满足性一致，而后者已知为 N2ExpTime 完全。作者采用类似构造，进一步证明无常量（三）守卫片段在带传递守卫时的有限可满足性是 2ExpTime 完全的。这些结果厘清了有限模型语义下相关逻辑的判定复杂度与模型规模界限。

问题
TGF 是表达能力很强的一阶可判定片段，但其有限可满足性及有限模型性质尚不明确。
方法
通过构造性模型论证证明 TGF 的有限模型性质，并给出模型大小的双指数上界；类似构造推广到带传递守卫的无常量（三）守卫片段。
评估
理论复杂性与模型规模界限分析：证明有限可满足性与可满足性一致（N2ExpTime 完全），并证明带传递守卫变体有限可满足性为 2ExpTime 完全。
原文摘要（Abstract）

The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6159,
  title = {Finite Model Theory of the Triguarded Fragment and Related Logics},
  author = {Emanuel Kieronski and Sebastian Rudolph},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470734}
}