Linear logic (LL) is very expressive: the smallest propositonal fragment is already NP-complete and the whole logic is indecidable. One can simulate usual computational models as many counters machines. The decidability of the fragment multiplicative exponential LL (MELL) is an open problem. This thesis establishes a correctness result for semi-linear phase semantics from the proof of the decidability of the accessibility in Petri nets. Indeed, the provability in some Horn fragment of MELL corresponds to this decision problem in the Petri nets. This result is a first step towards the decidability of MELL fragment (Y.Lafont conjecture). The next chapter describes an encoding of the hamiltonian circuits problem into the multiplicative LL (MLL). In this graph-theoretical problem, the additive notion of choice is viewed multiplicatively. This procedure may be used for other combinatorial problems. We obtain a new proof of the NP-completeness of MLL. M.Kanovich has established this result in 1992 using a reduction to 3-partition problem. But this reduction can not be used for the study of purely non-commutative fragment of MLL (this open problem needs another encoding). This is a joined work with T.Krantz. Finally we give a quadratic time correctness criterion for the proof nets of the non-commutative logic of P.Ruet. This logic contains LL and cyclic linear logic. Moreover we handle the case of proof nets with cuts.
