Kozen 模态μ演算公理化的完备性：一个简单证明
计算机科学中的逻辑
2020-10-20 v3 形式语言与自动机理论
计算机科学与博弈论
摘要
模态μ演算 (modal mu-calculus) 由 Dexter Kozen 提出，是带有不动点算子的模态逻辑扩展。其公理化系统 Koz 同时被提出，是最小模态逻辑 K 加上所谓的 Park 不动点归纳原理的扩展。Koz 的完备性证明耗时十余年，最终由 Igor Walukiewicz 完成。然而，他的证明相当复杂。在本文中，我们提出了一个改进的 Koz 完备性证明，虽然与原始证明相似，但更简单且易于理解。
引用
@article{arxiv.1408.3560,
title = {Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof},
author = {Kuniaki Tamura},
journal= {arXiv preprint arXiv:1408.3560},
year = {2020}
}