Connection Methods in Linear Logic and Proof Nets Construction Generation in Mixed Logics

Colloque sur invitation. internationale.International audienceWe study proof-search in mixed logics like the logic of Bunched Implications (BI) or Mixed Linear Logic (MLL), with the aim to build proofs or counter-models. We illustrate the different problems and some based-on semantics solutions from the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI is the basis of new foundations for Computer Science applications (logic programming, reasoning about mutable data structures). We present a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We then study the construction of tableaux and the extraction of countermodels from the proofs of completeness and of the finite model property. Relationships with proof-search methods in MLL are analyzed