Abstract
Linear Logic was introduced by Girard as a resource-sensitive refinement of classical logic. Linear Logic is of considerable interest for Computer Science. In this paper we focus on the correlations 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 a complete correspondence allows us to introduce several new semantics for Linear Logic and to clarify many results on the complexity of natural fragments of Linear Logic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S.Abramsky. Computational interpretation of linear logic. Imperial College Research Report DOC 90/20, 1990.
S.Abramsky, Computational Interpretations of Linear Logic, Theoretical Computer Science, 1992, Special Issue on the 1990 Workshop on Math. Found. Prog. Semantics. To appear.
S.Abramsky and R.Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic. Imperial College Technical Report DOC 92/24, 1992.
A.Asperti. A Logic for Concurrency. Technical Report. Dipartimento di Informatica, Universita di Pisa, 1987.
A.Asperti, G.-L.Ferrari, and R.Gorrieri. Implicative formulae in the’ proofs as computations’ analogy. In Proc. 17-th ACM Symposium on Principles of Programming Languages, San-Francisco, January 1990, p.59–71
J. van Benthem. Language in Action. North-Holland, Amsterdam, 1991.
A.Blass. A game semantics for linear logic. Annals Pure Appl. Logic, 56 (1992) pp.183–220.
A.Brown. Relating Petri Nets to Formulas of Linear Logic. Technical Report. LFCS, Edinburgh, 1989.
P.Degano, J.Meseguer, and U.Montanari. Axiomatizing net computations and processes. In Proc. 4-th Annual IEEE Symposium on Logic in Computer Science, Philadelphia, June 1989, p.175–185.
M.R.Garey and D.S.Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. 1979.
V.Gehlot and C.A.Gunter. Normal process representatives. In Proc. 5-th Annual IEEE Symposium on Logic in Computer Science, Philadelphia, June 1990.
J.-Y.Girard. Linear logic. Theoretical Computer Science, 50, 1–102, 1987.
J.-Y.Girard, A.Scedrov, and P.J.Scott, Bounded Linear Logic: A Modular Approach to Polynomial Time Computability, Theoretical Computer Science, 97:1–66, 1992.
C.A.Gunter and V.Gehlot. Nets as Tensor Theories. In Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn, 1989, p.174–191
M.I.Kanovich. The multiplicative fragment of Linear Logic is NP-complete. Technical Report X-91-13, University of Amsterdam, Institute for Language, Logic, and Information, June 1991
M.I.Kanovich. The Horn fragment of Linear Logic is NP-complete. Technical Report X-91-14, University of Amsterdam, Institute for Language, Logic, and Information, August 1991
M.I.Kanovich. Efficient program synthesis: Semantics, Logic, Complexity. Theoretical Aspects of Computer Software, TACS'91, Japan, Sendai, September 1991. In Lecture Notes in Computer Science, 526, p.615–632
M.I.Kanovich. Horn Programming in Linear Logic is NP-complete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, June 1992, pp.200–210
M.I.Kanovich. The complexity of Horn Fragments of Linear Logic, Annals Pure Appl. Logic, (1993) (to appear)
M.I.Kanovich. Linear Logic as a Logic of Computations, Annals Pure Appl. Logic, (1993) (to appear)
Y.Lafont and T.Streicher. Games semantics for linear logic. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, 43–51, Amsterdam, July 1991.
P.Lincoln, J.Mitchell, A.Scedrov, and N.Shancar. Decision Problems for Propositional Linear Logic. Technical Report SRI-CSL-90-08, CSL, SRI International, August 1990.
P.Lincoln, J.Mitchell, A.Scedrov, and N.Shankar. Decision Problems for Propositional Linear Logic. In Proc. 31st IEEE Symp. on Foundations of Computer Science, 662–671, 1990.
P.Lincoln, J.Mitchell, A.Scedrov, and N.Shankar. Decision Problems for Propositional Linear Logic. Annals Pure Appl. Logic, 56 (1992) pp. 239–311.
P.Lincoln, A.Scedrov, and N.Shancar. Linearizing Intuitionistic Implication. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, 51–62, Amsterdam, July 1991.
P.Lincoln and T.Winkler. Constant multiplicative Linear Logic is NP-complete. Draft, 1992.
N.Marti-Oliet and J.Mesequer. From Petri Nets to Linear Logic. In: Springer LNCS 389, ed. by D.R.Pitt et al., 1989, p.313–340
E.Mayr and A.Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46, 305–329, 1982.
E.Mayr, An algorithm for the general Petri net reachability problem. SIAM J.Comput., 13, N 3, 441–460, 1984.
J.Meseguer and U.Montanari. Petri Nets Are Monoids. Research Report SRI-CSL-88-3, SRI International, Menlo Park, January 1988.
M.Minsky. Recursive unsolvability of Post's problem of’ tag’ and other topics in the theory of Turing machines. Annals of Mathematics, 74:3:437–455, 1961.
V.R.Pratt, Event spaces and their linear logic, In AMAST'91: Algebraic Methodology and Software Technology, Iowa City, 1991, Workshops in Computing, 1–23, Springer-Verlag, 1992.
A.S.Troelstra, Lectures on Linear Logic, CSLI Lecture Notes No. 29, Center for the Study of Language and Information, Stanford University, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kanovich, M.I. (1994). Petri nets, Horn programs, Linear Logic, and vector games. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_119
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_119
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive