Sciweavers

TABLEAUX
2009
Springer

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

13 years 8 months ago
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.
Luis Pinto, Tarmo Uustalu
Added 27 Jul 2010
Updated 27 Jul 2010
Type Conference
Year 2009
Where TABLEAUX
Authors Luis Pinto, Tarmo Uustalu
Comments (0)