11 found
Order:
  1.  49
    2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
    Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  2.  15
    Cut Elimination for Extended Sequent Calculi.Simone Martini, Andrea Masini & Margherita Zorzi - 2023 - Bulletin of the Section of Logic 52 (4):459-495.
    We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  31
    A two‐dimensional metric temporal logic.Stefano Baratella & Andrea Masini - 2020 - Mathematical Logic Quarterly 66 (1):7-19.
    We introduce a two‐dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut elimination theorem down to formulas of a certain type.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  34
    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.
    We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  5.  31
    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  
  6.  16
    A Natural Deduction Calculus for S4.2.Simone Martini, Andrea Masini & Margherita Zorzi - 2024 - Notre Dame Journal of Formal Logic 65 (2):127-150.
    We propose a natural deduction calculus for the modal logic S4.2. The system is designed to match as much as possible the structure and the properties of the standard system of natural deduction for first-order classical logic, exploiting the formal analogy between modalities and quantifiers. The system is proved sound and complete with respect to (w.r.t.) the standard Hilbert-style formulation of S4.2. Normalization and its consequences are obtained in a natural way, with proofs that closely follow the analogous ones for (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7. A modal view of linear logic.Simone Martini & Andrea Masini - 1994 - Journal of Symbolic Logic 59 (3):888-899.
    We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  8. A note on unbounded metric temporal logic over dense time domains.Stefano Baratella & Andrea Masini - 2006 - Mathematical Logic Quarterly 52 (5):450-456.
    We investigate the consequences of removing the infinitary axiom and rules from a previously defined proof system for a fragment of propositional metric temporal logic over dense time.
    Direct download  
     
    Export citation  
     
    Bookmark  
  9.  26
    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  
  10.  26
    Back from the future.Andrea Masini, Luca Viganò & Marco Volpe - 2010 - Journal of Applied Non-Classical Logics 20 (3):241-277.
    Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  17
    Back from the future.Andrea Masini, Lucio Vigano & Marco Volpe - 2010 - Journal of Applied Non-Classical Logics 20 (3):241-277.
    Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation