一类时态逻辑的标记自然演绎系统
计算机科学中的逻辑
2008-03-25 v2
摘要
我们为扩展基本线性时态逻辑 Kl 的一类时态逻辑给出了标记自然演绎系统。我们证明了我们的系统相对于通常的 Kripke 语义是可靠且完备的，并且具有许多有用的归一化性质（特别是，推导可归约为享有子公式性质的正规形式）。我们还讨论了如何将我们的系统扩展以捕捉更丰富的逻辑，如（LTL 的片段）。
引用
@article{arxiv.0803.3187,
title = {Labeled Natural Deduction Systems for a Family of Tense Logics},
author = {Luca Viganò and Marco Volpe},
journal= {arXiv preprint arXiv:0803.3187},
year = {2008}
}