Switch to: References

Add citations

You must login to add citations.
  1. Temporal Gödel-Gentzen and Girard translations.Norihiro Kamide - 2013 - Mathematical Logic Quarterly 59 (1-2):66-83.
    A theorem for embedding a first-order linear- time temporal logic LTL into its intuitionistic counterpart ILTL is proved using Baratella-Masini's temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic. A substructural counterpart LLTL of ILTL is introduced, and a theorem for embedding ILTL into LLTL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic. These embedding theorems are proved syntactically based on Gentzen-type sequent calculi.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Combining linear-time temporal logic with constructiveness and paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
  • Bounded linear-time temporal logic: A proof-theoretic investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
  • Natural deduction calculi for classical and intuitionistic S5.S. Guerrini, A. Masini & M. Zorzi - 2023 - Journal of Applied Non-Classical Logics 33 (2):165-205.
    1. It is a fact that developing a good proof theory for modal logics is a difficult task. The problem is not in having deductive systems. In fact, all the main modal logics enjoy an axiomatic prese...
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • A natural deduction system for bundled branching time logic.Stefano Baratella & Andrea Masini - 2013 - Journal of Applied Non-Classical Logics 23 (3):268 - 283.
    We introduce a natural deduction system for the until-free subsystem of the branching time logic Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Strong Normalization of Program-Indexed Lambda Calculus.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (1/2):65-78.
    Direct download  
     
    Export citation  
     
    Bookmark