Resource Graphs and Countermodels in Resource Logics

Colloque avec actes et comité de lecture. internationale.International audienceIn this abstract we emphasize the role of a semantic structure called dependency graph in order to study the provability in some resource-sensitive logics, like the Bunched Implications Logic (BI) or the Non-commutative Logic (NL). Such a semantic structure is appropriate to capture the particular interactions between different kinds of connectives (additives and multiplicatives in BI and commutatives and non-commutatives in NL) during proof-search and mainly to provide countermodels in case of non-provability. We illustrate the key points with a tableau method for BI logic and present tools, namely BILL and CheckBI, dedicated for respectively countermodel generation and verification in this logic