paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Constructive completeness for the linear-time μ-calculus

线性时间 μ-演算的构造性完备性
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 该论文是线性时间 μ-演算的构造性完备性证明，属于纯逻辑与自动机理论，未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。虽然与形式化验证有间接关联，但与画像中关注的“LLM/Agent 改进形式化验证”或“程序分析”问题距离较远。引用 29 inbox
Amina Doumane
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：为线性时间 μ-演算的 Kozen 公理化给出构造性完备性证明，对每个有效公式构造证明。

本文研究线性时间 μ-演算相对于 Kozen 公理系统的完备性。作者给出一个新的构造性证明：该证明不是仅断言每个有效公式可证，而是显式地为每个有效公式构造出相应的证明。该构造性方法强化了完备性定理，并能为该逻辑的证明论性质提供更精细的理解。评估方式为数学证明论论证，未涉及实现或实验。

问题
本文关注线性时间 μ-演算相对于 Kozen 公理系统的完备性。
方法
给出一个新的完备性证明，其核心特征是构造性：对每个有效公式构造证明。
评估
通过证明论论证完成，未报告实现或实验评估。
原文摘要（Abstract）

We give a new proof of completeness for the linear-time μ-calculus w.r.t. Kozens's axiomatization. Our proof has the advantage of being constructive, i.e., it builds a proof for every valid formula.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{Doumane17,
  title = {Constructive completeness for the linear-time μ-calculus},
  author = {Amina Doumane},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005075}
}