Skip navigation
Skip navigation

A cut-free sequent calculus for bi-intuitionistic logic

Postniece (previously Buisman), Linda; Gore, Rajeev


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

CollectionsANU Research Publications
Date published: 2007
Type: Conference paper
Source: Proceedings of TABLEAUX 2007


File Description SizeFormat Image
01_Postniece (previously Buisman)_A_cut-free_sequent_calculus_2007.pdf451.67 kBAdobe PDF    Request a copy

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

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator