1.  41
    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  
  2.  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  
  3. 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.