The complexity of Horn fragments of Linear Logic

Annals of Pure and Applied Logic 69 (2-3):195-241 (1994)
  Copy   BIBTEX

Abstract

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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,388

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Linear logic as a logic of computations.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 67 (1-3):183-212.
Petri nets, Horn programs, Linear Logic and vector games.Max I. Kanovich - 1995 - Annals of Pure and Applied Logic 75 (1-2):107-135.
On NP-completeness in Linear Logic.Alexey P. Kopylov - 1995 - Annals of Pure and Applied Logic 75 (1-2):137-152.
The linear logic of multisets.A. Tzouvaras - 1998 - Logic Journal of the IGPL 6 (6):901-916.
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
Linear logic with fixed resources.Dmitry A. Archangelsky & Mikhail A. Taitslin - 1994 - Annals of Pure and Applied Logic 67 (1-3):3-28.
Fragments of language.Ian Pratt-Hartmann - 2004 - Journal of Logic, Language and Information 13 (2):207-223.
Interpolation in fragments of classical linear logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.

Analytics

Added to PP
2014-01-16

Downloads
37 (#640,129)

6 months
6 (#572,300)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Petri nets, Horn programs, Linear Logic and vector games.Max I. Kanovich - 1995 - Annals of Pure and Applied Logic 75 (1-2):107-135.
RASP and ASP as a fragment of linear logic.Stefania Costantini & Andrea Formisano - 2013 - Journal of Applied Non-Classical Logics 23 (1-2):49-74.
Linear logic automata.Max I. Kanovich - 1996 - Annals of Pure and Applied Logic 78 (1-3):147-188.
Towards NP – P via proof complexity and search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.

Add more citations

References found in this work

Lectures on Linear Logic.Anne Sjerp Troelstra - 1992 - Center for the Study of Language and Information Publications.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.

Add more references