An approach to infinitary temporal proof theory

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

Abstract
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
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 46,509
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.
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.
2-Sequent Calculus: A Proof Theory of Modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
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

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

Add more citations

Similar books and articles

Infinitary Modal Logic and Generalized Kripke Semantics.Pierluigi Minari - 2011 - Annali Del Dipartimento di Filosofia 17 (1):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.

Analytics

Added to PP index
2013-11-23

Total views
12 ( #693,794 of 2,286,502 )

Recent downloads (6 months)
1 ( #862,224 of 2,286,502 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature