一类时态逻辑的标号自然演绎系统
Labeled Natural Deduction Systems for a Family of Tense Logics
摘要：
我们给出了一类时态逻辑的标号自然演绎系统，它是对基本线性时态逻辑K1的扩充。我们证明，我们的系统是健全的和完整的，就通常的Kripke语义，他们拥有一些有用的规范化属性（特别是，派生减少到一个范式，享有子公式属性）。我们还讨论了如何扩展我们的系统，以捕获更丰富的逻辑，如（片段）LTL。
英文摘要：
We give labeled natural deduction systems for a family of tense logics extending the basic linear tense logic Kl. We prove that our systems are sound and complete with respect to the usual Kripke semantics, and that they possess a number of useful normalization properties (in particular, derivations reduce to a normal form that enjoys a subformula property). We also discuss how to extend our systems to capture richer logics like (fragments of) LTL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
