Results for 'Linear logic'

978 found
Order:
  1. A Comparison between two Different Tarski-style Semantics for Linear Logic.Linear Logic & M. Piazza - 1994 - Epistemologia 17 (1):101-116.
     
    Export citation  
     
    Bookmark  
  2.  14
    Classical linear logics with mix separation principle.Norihiro Kamide - 2003 - Mathematical Logic Quarterly 49 (2):201-209.
    Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut-elimination theorems, the completeness theorems and a characteristic property named the mix separation principle are proved for these logics.
    Direct download  
     
    Export citation  
     
    Bookmark  
  3.  27
    Linear logic in computer science.Thomas Ehrhard (ed.) - 2004 - New York: Cambridge University Press.
    Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  4.  4
    Linear Logic.Jean-Yves Girard - 1987 - Theoretical Computer Science 50:1–101.
    The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   134 citations  
  5.  25
    Local computation in linear logic.Ugo Solitro & Silvio Valentini - 1993 - Mathematical Logic Quarterly 39 (1):201-212.
    This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  6.  32
    Modeling linear logic with implicit functions.Sergey Slavnov - 2014 - Annals of Pure and Applied Logic 165 (1):357-370.
    Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations . However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  7.  24
    The linear logic of multisets.A. Tzouvaras - 1998 - Logic Journal of the IGPL 6 (6):901-916.
    We consider finite multisets over some set of urelements equipped only with additive union [uplus ] and show that the {[otimes], -0}-Horn fragment of Intuitionistic Linear Logic has a sound and complete interpretation in them by interpreting [otimes] as [uplus ]. The linear implication is interpreted by ordered pairs of multisets expressing replacement. The operator ! is also defined in an asymptotic way. Soundness, completeness and partial completeness results are proved for the {×, -0, !}-Horn fragment as (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  8. Golog and Linear Logic Programming.G. White - 1998 - Dept. Of Computer Science, Queen Mary and Westfield College.
    Levesque et al. have defined a programming language, Golog, in order to reason about complex actions within the framework of the situation calculus. We build on previous work of ours and show how to translate Golog into linear logic, suitably augmented.
     
    Export citation  
     
    Bookmark  
  9.  39
    Linear Logic and Lukasiewicz ℵ0- Valued Logic: A Logico-Algebraic Study.Jayanta Sen & M. K. Chakraborty - 2001 - Journal of Applied Non-Classical Logics 11 (3-4):313-329.
    A new characterization of all the MV-algebras embedded in a CL-algebra has been presented. A new sequent calculus for Lukasiewicz ℵ0-valued logic is introduced. Some links between this calculus and the sequent calculus for multiplicative additive linear logic are established. It has been shown that Lukasiewicz ℵ0-valued logic can be embedded in a suitable extension of MALL.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  10.  36
    Linear logic model of state revisited.V. de Paiva - 2014 - Logic Journal of the IGPL 22 (5):791-804.
    In an unpublished note Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model state manipulation via the notions of sequential composition and ‘regenerative values’. His calculus introduces the connective ‘before’ ▹ and an associated modality †, for the storage of objects sequentially reusable. Earlier and independently de Paiva introduced a (collection of) dialectica categorical models for (classical and intuitionistic) Linear Logic, the categories Dial2Set. These categories contain, apart (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11.  23
    Light linear logics with controlled weakening: Expressibility, confluent strong normalization.Max Kanovich - 2012 - Annals of Pure and Applied Logic 163 (7):854-874.
  12.  20
    Linear logic for nets with bounded resources.Dmitry A. Archangelsky, Mikhail I. Dekhtyar & Mikhail A. Taitslin - 1996 - Annals of Pure and Applied Logic 78 (1-3):3-28.
    In this paper we introduce a new type of nets with bounded types of distributed resources . Linear Logic to describe the behaviour of BR-nets is defined. It is based on Girard's Linear Logic but captures not only consumption of resources but their presence as well. Theorem of soundness and completeness of the proposed axiomatization is proved and the complexity of the provability problem is established for the general case and some particular ones.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  45
    Linear Logic and Intuitionistic Logic.Mitsuhiro Okada - 2004 - Revue Internationale de Philosophie 4:449-481.
  14.  11
    Lambda Calculus and Intuitionistic Linear Logic.Simona Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language Λ! and a categorical model (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  15. Linear Logic in Computer Science.P. Scott - 2006 - Bulletin of Symbolic Logic 12 (2):297-299.
  16.  36
    On NP-completeness in Linear Logic.Alexey P. Kopylov - 1995 - Annals of Pure and Applied Logic 75 (1-2):137-152.
    In this paper the questions remaining open about NP-completeness of multiplicative and Horn fragments of the Linear Logic and the Linear Logic with the weakening rule are answered.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  17. An algebraic investigation of Linear Logic.Paolo Aglianò - forthcoming - Archive for Mathematical Logic:1-23.
    In this paper we investigate two logics (and their fragments) from an algebraic point of view. The two logics are: MALL\textsf{MALL} (multiplicative-additive Linear Logic) and LL\textsf{LL} (classical Linear Logic). Both logics turn out to be strongly algebraizable in the sense of Blok and Pigozzi and their equivalent algebraic semantics are, respectively, the variety of Girard algebras and the variety of girales. We show that any variety of girales has a TD-term and hence equationally definable principal congruences. (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18. Modelling Combinatorial Auctions in Linear Logic.Daniele Porello & Ulle Endriss - 2010 - In Daniele Porello & Ulle Endriss, Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, {KR} 2010, Toronto, Ontario, Canada, May 9-13, 2010.
    We show that linear logic can serve as an expressive framework in which to model a rich variety of combinatorial auction mechanisms. Due to its resource-sensitive nature, linear logic can easily represent bids in combinatorial auctions in which goods may be sold in multiple units, and we show how it naturally generalises several bidding languages familiar from the literature. Moreover, the winner determination problem, i.e., the problem of computing an allocation of goods to bidders producing a (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  19.  44
    Quantized linear logic, involutive quantales and strong negation.Norihiro Kamide - 2004 - Studia Logica 77 (3):355-384.
    A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  20.  84
    Syllogisms in Rudimentary Linear Logic, Diagrammatically.Ruggero Pagnan - 2013 - Journal of Logic, Language and Information 22 (1):71-113.
    We present a reading of the traditional syllogistics in a fragment of the propositional intuitionistic multiplicative linear logic and prove that with respect to a diagrammatic logical calculus that we introduced in a previous paper, a syllogism is provable in such a fragment if and only if it is diagrammatically provable. We extend this result to syllogistics with complemented terms à la De Morgan, with respect to a suitable extension of the diagrammatic reasoning system for the traditional case (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  21.  91
    Full intuitionistic linear logic.Martin Hyland & Valeria de Paiva - 1993 - Annals of Pure and Applied Logic 64 (3):273-291.
    In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. This system is distinct from Classical Linear Logic, but unlike the standard Intuitionistic Linear Logic of Girard and Lafont includes the multiplicative disjunction par. This connective does have an entirely natural interpretation in a variety of categorical models of Intuitionistic Linear Logic. The main proof-theoretic problem arises from the observation of Schellinx (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  22. Modelling Multilateral Negotiation in Linear Logic.Daniele Porello & Ulle Endriss - 2010 - In Daniele Porello & Ulle Endriss, {ECAI} 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings. pp. 381--386.
    We show how to embed a framework for multilateral negotiation, in which a group of agents implement a sequence of deals concerning the exchange of a number of resources, into linear logic. In this model, multisets of goods, allocations of resources, preferences of agents, and deals are all modelled as formulas of linear logic. Whether or not a proposed deal is rational, given the preferences of the agents concerned, reduces to a question of provability, as does (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  23.  75
    Plans, actions and dialogues using linear logic.Lucas Dixon, Alan Smaill & Tracy Tsang - 2009 - Journal of Logic, Language and Information 18 (2):251-289.
    We describe how Intuitionistic Linear Logic can be used to provide a unified logical account for agents to find and execute plans. This account supports the modelling of agent interaction, including dialogue; allows agents to be robust to unexpected events and failures; and supports significant reuse of agent specifications. The framework has been implemented and several case studies have been considered. Further applications include human–computer interfaces as well as agent interaction in the semantic web.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  24.  89
    Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  25. Linear logic: its syntax and semantics.Jean-Yves Girard - 1995 - In Jean-Yves Girard, Yves Lafont & Laurent Regnier, Advances in linear logic. New York, NY, USA: Cambridge University Press. pp. 222--1.
     
    Export citation  
     
    Bookmark   30 citations  
  26.  91
    Linear logic proof games and optimization.Patrick D. Lincoln, John C. Mitchell & Andre Scedrov - 1996 - Bulletin of Symbolic Logic 2 (3):322-338.
    § 1. Introduction. Perhaps the most surprising recent development in complexity theory is the discovery that the class NP can be characterized using a form of randomized proof checker that only examines a constant number of bits of the “proof” that a string is in a language [6, 5, 31, 3, 4]. More specifically, writing ∣x∣ for the length of a string x, a language L in the class NP of languages recognizable in Nondeterministic polynomial time is traditionally given by (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark  
  27.  45
    Linear logic automata.Max I. Kanovich - 1996 - Annals of Pure and Applied Logic 78 (1-3):147-188.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  28. 1 NATO Science Committee Fakultat fiir Informatik, Technische Universitgt Mijnchen.M. Wirsing, Jp Jouannoud, A. Scedrov & Bounded Linear Logic - 1993 - Annals of Pure and Applied Logic 60:89.
     
    Export citation  
     
    Bookmark  
  29.  53
    Advances in linear logic.Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.) - 1995 - New York, NY, USA: Cambridge University Press.
    Linear logic, introduced in 1986 by J.-Y. Girard, is based upon a fine grain analysis of the main proof-theoretical notions of logic. The subject develops along the lines of denotational semantics, proof nets and the geometry of interaction. Its basic dynamical nature has attracted computer scientists, and various promising connections have been made in the areas of optimal program execution, interaction nets and knowledge representation. This book is the refereed proceedings of the first international meeting on (...) logic held at Cornell University, in June 1993. Survey papers devoted to specific areas of linear logic, as well as an extensive general introduction to the subject by J.-Y. Girard, have been added, so as to make this book a valuable tool both for the beginner and for the advanced researcher. (shrink)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  30.  30
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  31.  47
    Decision problems for propositional linear logic.Patrick Lincoln, John Mitchell, Andre Scedrov & Natarajan Shankar - 1992 - Annals of Pure and Applied Logic 56 (1-3):239-311.
    Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   43 citations  
  32.  81
    Curry-Howard terms for linear logic.Frank A. Bäuerle, David Albrecht, John N. Crossley & John S. Jeavons - 1998 - Studia Logica 61 (2):223-235.
    In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  33.  57
    Linear logic displayed.Nuel Belnap - 1989 - Notre Dame Journal of Formal Logic 31 (1):14-25.
  34.  16
    Sequent Systems for Consequence Relations of Cyclic Linear Logics.Paweł Płaczek - 2024 - Bulletin of the Section of Logic 53 (2):245-274.
    Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35.  33
    Sequent Calculi for Intuitionistic Linear Logic with Strong Negation.Norihiro Kamide - 2002 - Logic Journal of the IGPL 10 (6):653-678.
    We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third one is called a triple-context calculus, (...)
    Direct download  
     
    Export citation  
     
    Bookmark   11 citations  
  36.  44
    Linear logic with fixed resources.Dmitry A. Archangelsky & Mikhail A. Taitslin - 1994 - Annals of Pure and Applied Logic 67 (1-3):3-28.
    In this paper we continue the study of Girard's Linear Logic and introduce a new Linear Logic with modalities. Our logic describes not only the consumption, but also the presence of resources. We introduce a new semantics and a new calculus for this logic. In contrast to the results of Lincoln [7] and Kanovich [4] about the NP-completeness of the problem of the construction of a proof for a given sequent in the multiplicative fragment (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  37. Linear logic : A survey.J.-Y. Girard - 1995 - In Philippe De Groote, The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
     
    Export citation  
     
    Bookmark   6 citations  
  38.  11
    Computational Aspects of Linear Logic.Patrick Lincoln - 1995 - MIT Press.
  39.  26
    Linear logic.Roberto Di Cosmo & Dale Miller - unknown - Stanford Encyclopedia of Philosophy.
    , from Stanford Encyclopaedia of Philosophy.
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  40. Kripke models for linear logic.Gerard Allwein & J. Michael Dunn - 1993 - Journal of Symbolic Logic 58 (2):514-545.
    We present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutatively and associatively are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the logic (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   32 citations  
  41.  43
    Order algebras as models of linear logic.Constantine Tsinakis & Han Zhang - 2004 - Studia Logica 76 (2):201 - 225.
    The starting point of the present study is the interpretation of intuitionistic linear logic in Petri nets proposed by U. Engberg and G. Winskel. We show that several categories of order algebras provide equivalent interpretations of this logic, and identify the category of the so called strongly coherent quantales arising in these interpretations. The equivalence of the interpretations is intimately related to the categorical facts that the aforementioned categories are connected with each other via adjunctions, and the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  42. Simulation, Ramification, and Linear Logic.G. Graham White - 1998 - Linköping Electronic Articles in Computer and Information Science 3 (12).
     
    Export citation  
     
    Bookmark  
  43.  47
    Planar and braided proof-nets for multiplicative linear logic with mix.G. Bellin & A. Fleury - 1998 - Archive for Mathematical Logic 37 (5-6):309-325.
    We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear logic with Mix embedded in $R^3$ . (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  44.  59
    A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
    We present a game semantics in the style of Lorenzen for Girard's linear logic . Lorenzen suggested that the meaning of a proposition should be specified by telling how to conduct a debate between a proponent P who asserts and an opponent O who denies . Thus propositions are interpreted as games, connectives as operations on games, and validity as existence of a winning strategy for P. We propose that the connectives of linear logic can be (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   59 citations  
  45.  8
    Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic.Alexander V. Gheorghiu, Tao Gu & David J. Pym - forthcoming - Studia Logica:1-61.
    Proof-theoretic semantics (P-tS) is an innovative approach to grounding logical meaning in terms of proofs rather than traditional truth-conditional semantics. The point is not that one provides a proof system, but rather that one articulates meaning in terms of proofs and provability. To elucidate this paradigm shift, we commence with an introduction that contrasts the fundamental tenets of P-tS with the more prevalent model-theoretic approach to semantics. The contribution of this paper is a P-tS for a substructural logic, intuitionistic (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  46. Equality in linear logic.Marcelo E. Coniglio & Francisco Miraglia - 1996 - Logique Et Analyse 39 (153-154):113-151.
  47. Evolving algebras and light linear logic.Dean Rosenzweig - 1997 - Bulletin of Symbolic Logic 3.
  48.  32
    Non decomposable connectives of linear logic.Roberto Maieli - 2019 - Annals of Pure and Applied Logic 170 (11):102709.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  49.  57
    A note on full intuitionistic linear logic.G. M. Bierman - 1996 - Annals of Pure and Applied Logic 79 (3):281-287.
    This short note considers the formulation of Full Intuitionistic Linear Logic given by Hyland and de Paiva . Unfortunately the formulation is not closed under the process of cut elimination. This note proposes an alternative formulation based on the notion of patterns.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  50. Coherent obsessional experiments for linear logic proof-nets.Lorenzo Tortora de Falco - 2001 - Bulletin of Symbolic Logic 7 (1):154-171.
     
    Export citation  
     
    Bookmark  
1 — 50 / 978