A cut-free sequent calculus for bi-intuitionistic logic

Linda Buisman*, Rajeev Goré

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    15 Citations (Scopus)

    Abstract

    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.

    Original languageEnglish
    Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 16th International Conference, TABLEAUX 2007, Proceedings
    PublisherSpringer Verlag
    Pages90-106
    Number of pages17
    ISBN (Print)9783540730989
    DOIs
    Publication statusPublished - 2007
    Event16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007 - Aix en Provence, France
    Duration: 3 Jul 20076 Jul 2007

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume4548 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007
    Country/TerritoryFrance
    CityAix en Provence
    Period3/07/076/07/07

    Fingerprint

    Dive into the research topics of 'A cut-free sequent calculus for bi-intuitionistic logic'. Together they form a unique fingerprint.

    Cite this