7 février 2011
Daniel Mery (LORIA)We present a new characterisation of validity in propositional bi-intuitionistic logic in terms of specific graphical structures called “resource graphs”. Such resource graphs not only take into account the essential operational aspects of a proof-search process but also include semantic aspects in order to enable countermodel construction in the case of non-validity. As a consequence, a key and original feature of resource graphs is that they can be indifferently understood from either a proof, or a refutation point of view. In this talk, we illustrate the usefulness of resource graphs by using them as a tool for defining a new connection-based characterisation of propositional bi-intuitionistic validity from which we then derive a sound and complete free-variable labelled sequent calculus that also admits cut-elimination and variable splitting.