9 found
Order:
  1.  37
    Display to Labeled Proofs and Back Again for Tense Logics.Agata Ciabattoni, Tim Lyon, Revantha Ramanayake & Alwen Tiu - 2021 - ACM Transactions on Computational Logic 22 (3):1-31.
    We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  2. From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
    We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  3.  17
    Hypersequent and Display Calculi – a Unified Perspective.Agata Ciabattoni, Revantha Ramanayake & Heinrich Wansing - 2014 - Studia Logica 102 (6):1245-1294.
    This paper presents an overview of the methods of hypersequents and display sequents in the proof theory of non-classical logics. In contrast with existing surveys dedicated to hypersequent calculi or to display calculi, our aim is to provide a unified perspective on these two formalisms highlighting their differences and similarities and discussing applications and recent results connecting and comparing them.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  4.  49
    Valentini’s Cut-Elimination for Provability Logic Resolved.Rajeev Goré & Revantha Ramanayake - 2012 - Review of Symbolic Logic 5 (2):212-238.
    In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There is (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  5.  4
    Labelled Tree Sequents, Tree Hypersequents and Nested Sequents.Rajeev Goré & Revantha Ramanayake - 2012 - In Thomas Bolander, Torben Braüner, Silvio Ghilardi & Lawrence Moss (eds.), Advances in Modal Logic, Volume 9. CSLI Publications. pp. 279-299.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  29
    Cut-Elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
    We present a syntactic proof of cut-elimination for weak Grzegorczyk logic Go. The logic has a syntactically similar axiomatisation to Gödel–Löb logic GL (provability logic) and Grzegorczyk’s logic Grz. Semantically, GL can be viewed as the irreflexive counterpart of Go, and Grz can be viewed as the reflexive counterpart of Go. Although proofs of syntactic cut-elimination for GL and Grz have appeared in the literature, this is the first proof of syntactic cut-elimination for Go. The proof is technically interesting, requiring (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  2
    Bounded-Analytic Sequent Calculi and Embeddings for Hypersequent Logics.Agata Ciabattoni, Timo Lang & Revantha Ramanayake - 2021 - Journal of Symbolic Logic 86 (2):635-668.
    A sequent calculus with the subformula property has long been recognised as a highly favourable starting point for the proof theoretic investigation of a logic. However, most logics of interest cannot be presented using a sequent calculus with the subformula property. In response, many formalisms more intricate than the sequent calculus have been formulated. In this work we identify an alternative: retain the sequent calculus but generalise the subformula property to permit specific axiom substitutions and their subformulas. Our investigation leads (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8.  13
    Non-Commutative Classical Arithmetical Sequent Calculi Are Intuitionistic.Revantha Ramanayake - 2016 - Logic Journal of the IGPL 24 (3):441-452.
  9.  3
    Valentini's Cut-Elimination for Provability Logic Resloved.Rajeev Goré & Revantha Ramanayake - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 67-86.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation