We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

An embedding of the implicational propositional intuitionistic logic into the nonmodal fragment of intuitionistic linear logic is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs.

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)

, from Stanford Encyclopaedia of Philosophy.