Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic
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]
|Collections||ANU Research Publications|
|Source:||Journal of Logic and Computation|
|01_Gore_Combining_Derivations_and_2008.pdf||315.49 kB||Adobe PDF||Request a copy|
|02_Gore_Combining_Derivations_and_2008.pdf||373.89 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.