The question at issue is to develop a computational interpretation of Girard's Linear Logic [Girard, 1987] and to obtain efficient decision algorithms for this logic, based on the bottom-up approach. It involves starting with the simplest natural fragment of linear logic and then expanding it step-by-step. We give a complete computational interpretation for the Horn fragment of Linear Logic and some natural generalizations of it enriched by the two additive connectives: and &. Within the framework of this interpretation, it becomes (...) possible to explicitly formalize and clarify the computational aspects of the fragments of Linear Logic in question and establish exactly the complexity level of these fragments. In particular, the simplest natural Horn fragment of Linear Logic is proved to be NP-complete. As a corollary, we obtain the affirmative solution for the problem ): whether the multiplicative fragment of linear logic is NP-complete. (shrink)

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 is proved to be simulated directly within the framework of each of these systems. (shrink)

The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, and the modal storage operator !. We give a complete computational interpretation for the !-Horn (...) fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known ‘ or ’-like connective ⊕, and, for the sake of the computational duality, we introduce a new ‘ and ’-like connective @ For !-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the -Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, the modal storage operator!, and the additive ‘disjunction’ ⊕, we prove that standard Minsky machines [21] can be directly encoded in this -Horn fragment. Standard Minsky machines can be directly encoded in the corresponding ‘dual’ -Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable. (shrink)

In the original publication, the affiliation of the author Max Kanovich was processed incorrectly. It has been updated in this correction.

A Linear Logic automaton is a hybrid of a finite automaton and a non-deterministic Petri net. LL automata commands are represented by propositional Horn Linear Logic formulas. Computations performed by LL automata directly correspond to cut-free derivations in Linear Logic.A programming language of LL automata is developed in which typical sequential, non-deterministic and parallel programming constructs are expressed in the natural way.All non-deterministic computations, e.g. computations performed by programs built up of guarded commands in the Dijkstra's approach to non-deterministic programming, (...) are directly simulated within the framework of Linear Logic automata, and thereby within the Horn framework of Linear Logic. (shrink)

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut. We also prove algorithmic undecidability for both (...) calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (shrink)