paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting

为带计数的守卫二变量片段添加路径函数依赖
LMCS vol.Volume 13, Issue 42017匹配度 2/10 · 该论文属于纯逻辑与数据库理论，研究守卫片段、计数与路径函数依赖的可满足性复杂度，与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接交叉。虽然形式化理论可能与形式化验证有间接关联，但不涉及程序分析或 Agentic 系统。引用 1 inbox
Georgios Kourtis, Ian Pratt-Hartmann
逻辑与自动机
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：证明加入路径函数依赖与数据库后，带计数量词的守卫二变量片段的可满足性与有限可满足性均为 ExpTime 完全。

论文研究一阶逻辑中带计数量词的守卫二变量片段，并将其扩展以包含数据库与路径函数依赖。路径函数依赖可表达类似键约束的函数性依赖，可能影响该逻辑片段的判定行为。作者考察该扩展逻辑下可满足性与有限可满足性问题的计算复杂度，证明二者均为 ExpTime 完全。该结果界定了这一片段在数据库与知识表示场景中的推理代价，说明加入计数量词与路径函数依赖后，判定问题仍具有 ExpTime 完全复杂度。

问题
研究带计数量词的守卫二变量一阶片段在加入数据库与路径函数依赖后，其可满足性和有限可满足性的判定复杂度。
方法
将路径函数依赖纳入带计数量词的守卫二变量片段的逻辑框架，并对可满足性与有限可满足性判定问题进行复杂度分析。
评估
通过复杂度理论证明，得到可满足性与有限可满足性两个判定问题均为 ExpTime 完全的结论。
原文摘要（Abstract）

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.

链接与引用

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

BibTeX 
@article{KourtisP16,
  title = {Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting},
  author = {Georgios Kourtis and Ian Pratt-Hartmann},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 4},
  year = {2017},
  doi = {10.23638/lmcs-13(4:4)2017}
}