A Connection-based Characterization of Bi-intuitionistic Validity

International audienceWe give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting