TY - GEN
T1 - A cut-free sequent calculus for bi-intuitionistic logic
AU - Buisman, Linda
AU - Goré, Rajeev
PY - 2007
Y1 - 2007
N2 - 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 interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees. Our simple termination argument allows our calculus to be used for automated deduction, although this is not its main purpose.
AB - 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 interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees. Our simple termination argument allows our calculus to be used for automated deduction, although this is not its main purpose.
UR - http://www.scopus.com/inward/record.url?scp=37249065328&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73099-6_9
DO - 10.1007/978-3-540-73099-6_9
M3 - Conference contribution
SN - 9783540730989
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 90
EP - 106
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 16th International Conference, TABLEAUX 2007, Proceedings
PB - Springer Verlag
T2 - 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007
Y2 - 3 July 2007 through 6 July 2007
ER -