Skip navigation
Skip navigation

Cut-elimination and proof-search for bi-intutionistic logic using nested sequents

Gore, Rajeev; Postniece (previously Buisman), Linda; Tiu, Alwen


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,...[Show more]

CollectionsANU Research Publications
Date published: 2008
Type: Conference paper
Source: Advances in Modal Logic, Volume 7


File Description SizeFormat Image
01_Gore_Cut-elimination_and_2008.pdf408.73 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator