Switch to: References

Add citations

You must login to add citations.
  1. Petri nets, Horn programs, Linear Logic and vector games.Max I. Kanovich - 1995 - Annals of Pure and Applied Logic 75 (1-2):107-135.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Towards NP – P via proof complexity and search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The complexity of Horn fragments of Linear Logic.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 69 (2-3):195-241.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
    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.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Linear logic as a logic of computations.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 67 (1-3):183-212.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • A modal view of linear logic.Simone Martini & Andrea Masini - 1994 - Journal of Symbolic Logic 59 (3):888-899.
    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.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Linear logic.Roberto Di Cosmo & Dale Miller - unknown - Stanford Encyclopedia of Philosophy.
    , from Stanford Encyclopaedia of Philosophy.
    Download  
     
    Export citation  
     
    Bookmark   4 citations