Skip navigation
Skip navigation

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

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

Description

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
URI: http://hdl.handle.net/1885/52679
Source: Advances in Modal Logic, Volume 7
DOI: 10.1.1.218.5308

Download

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:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator