带逆模态的平坦模态不动点逻辑
计算机科学中的逻辑
2017-10-13 v1
摘要
我们证明了对应于双向 mu-演算平坦片段的一类模态不动点逻辑的通用完备性结果，扩展了 Santocanale 和 Venema 的早期工作。我们观察到，Santocanale 和 Venema 使用有限伴随证明了某些平坦不动点逻辑的 Lindenbaum-Tarski 代数中的最小不动点是构造性的，但当引入逆模态时，该证明不再有效。相反，我们的完备性证明直接为一致公式构造了一个模型，其使用归纳规则的方式类似于命题动态逻辑的标准完备性证明。该方法与焦点的概念相结合，该概念此前已被用于模态不动点逻辑的基于 tableau 的推理中。
引用
@article{arxiv.1710.04628,
title = {Flat modal fixpoint logics with the converse modality},
author = {Sebastian Enqvist},
journal= {arXiv preprint arXiv:1710.04628},
year = {2017}
}