A cut-free sequent calculus for bi-intuitionistic logic
Postniece (previously Buisman), Linda; Gore, Rajeev
Description
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]
Collections | ANU Research Publications |
---|---|
Date published: | 2007 |
Type: | Conference paper |
URI: | http://hdl.handle.net/1885/51986 |
Source: | Proceedings of TABLEAUX 2007 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Postniece (previously Buisman)_A_cut-free_sequent_calculus_2007.pdf | 451.67 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator