Proof-search and Proof Nets in Mixed Linear Logic

AbstractIn this paper we study how to design proof-search methods for the multiplicative fragment of Mixed Linear Logic which combines both commutative and noncommutative connectives. After an analysis of the interaction and relationships between these connectives, we propose two different proof-search algorithms, both based on the construction of labelled proof nets. The labels allow in the former to fix some constraints to satisfy during the proof net search and in the latter to propagate some informations useful to guide and control the search. Such based-on proof nets methods are useful to efficiently detect the non-provability and could lead to the generation of some countermodels