4 found
  1.  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  
  2.  47
    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  
  3.  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  
  4.  13
    Non-Commutative Classical Arithmetical Sequent Calculi Are Intuitionistic.Revantha Ramanayake - 2016 - Logic Journal of the IGPL 24 (3):441-452.