paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Unary negation fragment with equivalence relations has the finite model property

带等价关系的一元否定片段具有有限模型性质
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文研究一元否定片段加等价关系的有限模型性质与可满足性复杂度，属于纯逻辑/自动机理论，与用户关注的 float/贝叶斯程序分析、LLM/Agent 驱动的静态分析与形式化验证没有直接交集。它最多只与形式化验证的底层逻辑基础有非常间接的联系。引用 0 inbox
Daniel Danielski, Emanuel Kieroński
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明带任意多等价关系的一元否定片段具有有限模型性质，并确定其可满足性为 2-ExpTime 完全。

本文研究一阶逻辑一元否定片段（UNF）的扩展：允许任意多个二元符号被解释为等价关系。作者证明该扩展具有有限模型性质，并给出小模型上界：每个可满足公式都有一个规模至多双指数的模型。据此，他们确定该逻辑的可满足性问题（等价于有限可满足性）是 2-ExpTime 完全的。论文还将这些结果迁移到一个带等价关系的受限 guarded negation fragment 变体。

问题
研究一元否定片段在允许任意多个二元符号解释为等价关系后的可满足性、有限模型性质与复杂度。
方法
通过证明可满足公式具有规模至多双指数的小模型，从而建立有限模型性质，并分析可满足性问题的复杂度上下界。
评估
理论证明可满足性与有限可满足性等价且为 2-ExpTime 完全，并将结果推广到带等价关系的受限 guarded negation fragment。
原文摘要（Abstract）

We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is 2-ExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.

链接与引用

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

BibTeX 
@inproceedings{paperbot4375,
  title = {Unary negation fragment with equivalence relations has the finite model property},
  author = {Daniel Danielski and Emanuel Kieroński},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209205}
}