Skip navigation
Skip navigation

Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic

Gore, Rajeev; Postniece (previously Buisman), Linda


Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent 'cut-free' sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic...[Show more]

CollectionsANU Research Publications
Date published: 2008
Type: Journal article
Source: Journal of Logic and Computation
DOI: 10.1093/logcom/exn067


File Description SizeFormat Image
01_Gore_Combining_Derivations_and_2008.pdf315.49 kBAdobe PDF    Request a copy
02_Gore_Combining_Derivations_and_2008.pdf373.89 kBAdobe PDF    Request a copy

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

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator