Full-text resources of PSJD and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

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.