Combining linear-time temporal logic with constructiveness and paraconsistency
Combining linear-time temporal logic with constructiveness and paraconsistency
复制标题
将线性时间时序逻辑与构造性和准一致性相结合
DOI：
10.1016/j.jal.2009.06.001
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
H. Wansing
中科院分区：
文献类型：
--
作者：
N. Kamide;H. Wansing
线性时间时态逻辑（LTL）是经典逻辑的一种扩展，在表达计算机科学中研究的时态推理方面非常有用。本文引入了直觉逻辑或纳尔逊次协调逻辑的两种构造型和有界型LTL，作为Gentzen型演算。这些逻辑，IB[1]和PB[1]，旨在提供一个有用的理论基础，不仅表示时间（线性时间），但也建设性的，和次协调（不一致容忍）推理。所提出的逻辑的时域是有界的一个固定的正整数。尽管在时间域上受到限制，但逻辑可以导出LTL的几乎所有典型时间公理。作为有界时间的一个优点，我们分别证明了IB[1]和PB[1]的直觉逻辑和纳尔逊的次协调逻辑的忠实嵌入.作为本文的主要结果，证明了新定义的逻辑的完备性（相对于Kripke语义），割消，规范化（相对于自然演绎）和可判定性定理。此外，我们还对IB[1]和PB[1]给出了可靠而完整的显示结石.在[P. Maier，Intuitionistic LTL and a new characterization of safety and liveness，in：Proceedings of Computer Science Logic 2004，in：Lecture Notes in Computer Science，vol.3210，Springer-Verlag，柏林，2004，pp. 295-309]已经强调，直觉线性时间逻辑（ILTL）允许安全性和活性性质的优雅表征。系统ILTL，然而，已经提出了只有在一个代数设置。本文是第一个语义和证明理论研究的有界建设性的线性时间时态逻辑包含直觉或强否定。
It is known that linear-time temporal logic (LTL), which is an extension of classical logic, is useful for expressing temporal reasoning as investigated in computer science. In this paper, two constructive and bounded versions of LTL, which are extensions of intuitionistic logic or Nelson's paraconsistent logic, are introduced as Gentzen-type sequent calculi. These logics, IB[l] and PB[l], are intended to provide a useful theoretical basis for representing not only temporal (linear-time), but also constructive, and paraconsistent (inconsistency-tolerant) reasoning. The time domain of the proposed logics is bounded by a fixed positive integer. Despite the restriction on the time domain, the logics can derive almost all the typical temporal axioms of LTL. As a merit of bounding time, faithful embeddings into intuitionistic logic and Nelson's paraconsistent logic are shown for IB[l] and PB[l], respectively. Completeness (with respect to Kripke semantics), cut–elimination, normalization (with respect to natural deduction), and decidability theorems for the newly defined logics are proved as the main results of this paper. Moreover, we present sound and complete display calculi for IB[l] and PB[l]. In [P. Maier, Intuitionistic LTL and a new characterization of safety and liveness, in: Proceedings of Computer Science Logic 2004, in: Lecture Notes in Computer Science, vol. 3210, Springer-Verlag, Berlin, 2004, pp. 295–309] it has been emphasized that intuitionistic linear-time logic (ILTL) admits an elegant characterization of safety and liveness properties. The system ILTL, however, has been presented only in an algebraic setting. The present paper is the first semantical and proof-theoretical study of bounded constructive linear-time temporal logics containing either intuitionistic or strong negation.
登录
查看更多内容
DOI：
--
发表时间：
1996
期刊：
影响因子：
--
作者：
S. Martini;A. Masini
通讯作者：
A. Masini
带注释的时间逻辑 Delta*tau
DOI：
--
发表时间：
2000
期刊：
IBERAMIA-SBIA
影响因子：
--
作者：
J. Abe;S. Akama
通讯作者：
S. Akama
逻辑分析与综合
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
D. Gabbay;W. Carnieli;M. Coniglio;P. Gouveia;C. Sernadas
通讯作者：
C. Sernadas
结合时间分析的时间逻辑方法
DOI：
--
发表时间：
1995
期刊：
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Rowan Davies
通讯作者：
Rowan Davies
DOI：
--
发表时间：
1993
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
H. Wansing
通讯作者：
H. Wansing