期刊
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING
卷 76, 期 2, 页码 216-225出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlap.2008.02.004
关键词
sequent calculus; temporal logic; cut-free
类别
-
Currently known sequent systems for temporal logics such as linear time temporal logic and computation tree logic either rely on a cut rule, an invariant rule, Or an infinitary rule. The first and second violate the subformula property and the third has infinitely many premises. We present finitary cut-free invariant-free weakening-free and contraction-free sequent systems for both logics mentioned. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics. (C) 2008 Elsevier Inc. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据