Order:
  1.  67
    Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic Via Nested Sequents.Tim Lyon, Alwen Tiu, Rajeev Gore & Ranald Clouston - 2020 - In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Dagstuhl, Germany: pp. 1-16.
    We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  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  
  3.  5
    Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures.Alwen Tiu, Egor Ianovski & Rajeev Goré - 2012 - In Thomas Bolander, Torben Braüner, Silvio Ghilardi & Lawrence Moss (eds.), Advances in Modal Logic, Volume 9. CSLI Publications. pp. 516-537.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  4.  42
    Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66.
    We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  3
    Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic.Rajeev Goré, Linda Postniece & Alwen Tiu - 2010 - In Lev Beklemishev, Valentin Goranko & Valentin Shehtman (eds.), Advances in Modal Logic, Volume 8. CSLI Publications. pp. 156-177.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  6. John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge, UK, 2009, Xix + 681 Pp. [REVIEW]Alwen Tiu - 2010 - Bulletin of Symbolic Logic 16 (2):279-281.
  7.  5
    Cut Elimination for a Logic with Induction and Co-Induction.Alwen Tiu & Alberto Momigliano - 2012 - Journal of Applied Logic 10 (4):330-367.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation