Petri nets, Horn programs, Linear Logic and vector games Original Research Article

Linear Logic was introduced by Girard as a resource-sensitive refinement of classical logic. In this paper we establish strong connections between natural fragments of Linear Logic and a number of basic concepts related to different branches of Computer Science such as Concurrency Theory, Theory of Computations, Horn Programming and Game Theory. In particular, such complete correlations allow us to introduce several new semantics for Linear Logic and to clarify many results on the complexity of natural fragments of Linear Logic. As a main corollary, any non-deterministic and concurrent computation (e.g., computations performed by non-deterministic Minsky machines) is proved to be simulated directly within the framework of each of these systems.