Skip navigation
Skip navigation

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

Gore, Rajeev; Postniece (previously Buisman), Linda

Description

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
URI: http://hdl.handle.net/1885/52605
Source: Journal of Logic and Computation
DOI: 10.1093/logcom/exn067

Download

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