无交替 $\mu$-演算的聚焦式证明系统与插值
计算机科学中的逻辑
2021-05-04 v2
摘要
本文引入模态 -演算无交替片段的无切割相继式演算。该系统允许循环证明，并使用简单的聚焦机制来控制无限分支上不动点的展开。我们证明了该证明系统的可靠性与完备性，并应用它证明无交替片段具有 Craig 插值性质。
引用
@article{arxiv.2103.01671,
title = {Focus-style proof systems and interpolation for the alternation-free $\mu$-calculus},
author = {Johannes Marti and Yde Venema},
journal= {arXiv preprint arXiv:2103.01671},
year = {2021}
}