Cut-elimination and proof-search for bi-intutionistic logic using nested sequents
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]
|Collections||ANU Research Publications|
|Source:||Advances in Modal Logic, Volume 7|
|01_Gore_Cut-elimination_and_2008.pdf||408.73 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.