Archive for Mathematical Logic 43 (8):965-990 (2004)

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness
Keywords Proof theory  Sequent calculus  Infinitary logic  Cut elimination  Modal logic
Categories (categorize this paper)
DOI 10.1007/s00153-004-0237-z
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 60,021
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

An Axiomatization of Full Computation Tree Logic.M. Reynolds - 2001 - Journal of Symbolic Logic 66 (3):1011-1057.
A Model Existence Theorem in Infinitary Propositional Modal Logic.Krister Segerberg - 1994 - Journal of Philosophical Logic 23 (4):337 - 367.
2-Sequent Calculus: A Proof Theory of Modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
A Proof-Theoretic Investigation of a Logic of Positions.Stefano Baratella & Andrea Masini - 2003 - Annals of Pure and Applied Logic 123 (1-3):135-162.
Labelled Modal Logics: Quantifiers. [REVIEW]David Basin, Seán Matthews & Luca Viganò - 1998 - Journal of Logic, Language and Information 7 (3):237-263.

View all 6 references / Add more references

Citations of this work BETA

Bounded Linear-Time Temporal Logic: A Proof-Theoretic Investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
Temporal Gödel-Gentzen and Girard Translations.Norihiro Kamide - 2013 - Mathematical Logic Quarterly 59 (1-2):66-83.

Add more citations

Similar books and articles

Infinitary Modal Logic and Generalized Kripke Semantics.Pierluigi Minari - 2011 - Annali Del Dipartimento di Filosofia 17:135-166.
Kripke Completeness of Infinitary Predicate Multimodal Logics.Yoshihito Tanaka - 1999 - Notre Dame Journal of Formal Logic 40 (3):326-340.
Deep Sequent Systems for Modal Logic.Kai Brünnler - 2009 - Archive for Mathematical Logic 48 (6):551-577.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Admissibility of Cut in Congruent Modal Logics.Andrzej Indrzejczak - 2011 - Logic and Logical Philosophy 20 (3):189-203.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
The Cost of a Cycle is a Square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.


Added to PP index

Total views
12 ( #769,560 of 2,433,538 )

Recent downloads (6 months)
1 ( #468,801 of 2,433,538 )

How can I increase my downloads?


My notes