双直觉主义稳定时态逻辑的强完全性与有穷模型性质
计算机科学中的逻辑
2017-03-08 v1 逻辑
摘要
双直觉主义稳定时态逻辑（BIST 逻辑）是一类时态逻辑，其 Kripke 语义中的框架世界配备了一个预序以及一个关于该预序“稳定”的可通达关系。BIST 逻辑是逻辑 BiSKt 的扩张，后者产生于超图的语义背景，因为预序的一种特例可以表示超图的关联结构。本文首次给出了 BiSKt 的 Hilbert 式公理化，并证明了 BiSKt 的强完全性。我们进一步证明了通过特定形式的公式扩张 BiSKt 所得到的一类 BIST 逻辑的强完全性。此外，我们证明了一类 BIST 逻辑具有有穷模型性质和可判定性。
引用
@article{arxiv.1703.02198,
title = {Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics},
author = {Katsuhiko Sano and John G. Stell},
journal= {arXiv preprint arXiv:1703.02198},
year = {2017}
}
备注
In Proceedings M4M9 2017, arXiv:1703.01736