PL EN


Preferences help
enabled [disable] Abstract
Number of results
2012 | 47 |
Article title

Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic

Authors
Content
Title variants
Languages of publication
PL
Abstracts
PL
Linear-time temporal logics (LTLs) are known to be useful for verifying concurrent systems, and a simple natural deduction framework for LTLs has been required to obtain a good computational interpretation. In this paper, a typed -calculus B[l] with a Curry-Howard correspondence is introduced for an in-tuitionistic bounded linear-time temporal logic B[l], of which the time domain is bounded by a fixed positive integer l. The strong normalization theorem for B[l] is proved as a main result. The base logic B[l] is defined as a Gentzen-type sequent calculus, and despite the restriction on the time domain, B[l] can derive almost all the typical temporal axioms of LTLs. The proposed frame-work allows us to obtain a uniform and simple proof-theoretical treatment of both natural deduction and sequent calculus, i.e., the equivalence between them, the cut-elimination theorem, the decidability theorem, the Curry-Howard correspondence and the strong normalization theorem can be obtained uniformly.
Keywords
PL
 
Publisher
Year
Volume
47
Physical description
Dates
published
2012
online
07 - 07 - 2015
Contributors
References
Document Type
Publication order reference
Identifiers
YADDA identifier
bwmeta1.element.ojs-issn-2084-2589-year-2012-volume-47-article-2889
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.