Labelled Structures and Provability in Resource Logics - extended abstract

We emphasize the interest of labelled structures for analyzing provability in some resource logics. Labels and constraints allow to capture the semantic consequence relation in logics, like BI logic that combines intuitionistic and linear connectives. They provide new methods in proof theory which are based on specific structures, namely dependency graphs or labelled proof nets. Such semantic structures are central for the analysis of provability and the generation of proofs or countermodels. Knowing that BI is conservative w.r.t. Multiplicative Intuitionistic Linear Logic (MILL), we consider MILL from the BI perspective and show how labelled proof structures can provide a new based-on connection characterization of MILL provability. We also provide an algorithm that builds MILL proof nets and its related connection method based on labelled structures and constraints. The generation of proofs and countermodels is analyzed in this context