Proof net editor

Abstract EN

Linear logic (LL) [9], [10] (see Appendix A, B) is the logical foundation of some type theoretic languages and also of environments for specification and theorem proving.

In this paper, we consider the Multiplicative fragment of Linear Logic (MLL) from an automated deduction point of view.

We propose an automated deduction (Automatic Proof Nets Construction and its implementation) based on the notation of Proof net [Gir1995b] that is a semantic structure from which one can give a counterpart of natural deduction in linear logic.

Proof nets can be also seen as a multiple conclusion natural deduction system for linear logic and is a good formalism to analyses some computation mechanisms, for instant in type-theoretic interpretations.