9 found
Order:
  1.  16
    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   6 citations  
  2.  15
    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   8 citations  
  3. 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  
  4. 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 (3 more)  
     
    Export citation  
     
    Bookmark  
  5.  11
    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   2 citations  
  6.  1
    A Two‐Dimensional Metric Temporal Logic.Stefano Baratella & Andrea Masini - forthcoming - Mathematical Logic Quarterly.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7.  16
    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  
  8.  9
    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  
  9.  6
    Back From the Future.Andrea Masini, Lucio Vigano & Marco Volpe - 2010 - Journal of Applied Non-Classical Logics 20 (3):241-277.