Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents

Abstract. Bi-intuitionistic logic is a conservative extension of intuitionistic logic with a connective dual to implication, called exclusion. We present a sound and complete cut-free labelled sequent calculus for bi-intuitionistic propositional logic, BiInt, following S. Negri’s general method for devising sequent calculi for normal modal logics. Although it arises as a natural formalization of the Kripke semantics, it is does not directly support proof search. To describe a proof search procedure, we develop a more algorithmic version that also allows for counter-model extraction from a failed proof attempt.

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Luis Pinto, Tarmo Uustalu
• Keywords: Bi-intuitionistic Propositional Logic, Proof Search, Proof Search Procedure, TABLEAUX 2009