The complexity of Horn fragments of linear logic
type: Item
instance of: scholarly article
title: The complexity of Horn fragments of linear logic
zbMATH Open document ID: 0812.03007
DOI: 10.1016/0168-0072(94)90085-X
author: Max Kanovich
published in: Annals of Pure and Applied Logic
publication date: 1995-05-16T00:00:00Z
review text: Complexity of derivability for some Horn fragments of Girard's Linear Logic is considered. The first fragment consists of sequents with left parts of the form \(X\), \(S\) and right parts of the form \(Y\), where \(X\) and \(Y\) are multiplicative conjunctions of propositional variables (simple products), and \(S\) is a multiset of linear implications of simple products (simple Horn implications). The second, third and fourth fragement differ from the first by allowing \(S\) to include additive conjunctions of simple Horn implications, implications whose conclusions are additive disjunctions of simple products, and both of them, respectively. Variants of these fragments for Linear Logic with Weakening Rule are also considered. It is proved that the derivability problem for the first and second fragment (with and without Weakening Rule) and the third fragment (without Weakening Rule) is NP-complete, and for the other cases is PSPACE-complete. The proofs use some calculus HLL specialized for derivations of sequents in these fragments and some computational interpretations for derivability in these fragments based on HLL. It should be noted that the inductive proof of completeness of HLL (Theorem 2.10) is not accurate enough and should be carried out more carefully. Some notational conventions of Table 1 are sometimes not consistently used (e.g., an empty \(V\) should be allowed in the second rule of Table 3; see also the use of symbols \(A\), \(B\), \(C\) in Table 2). Commutativity Rule for comma is implicitly assumed in Table 2 with rules of Intuitionistic Linear Logic. Only Horn programs of tree-like form are really used in the paper rather than those of arbitrary acyclic graph form, as defined in Definition 3.1, whose semantics is not quite clear.
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 683707
zbMATH Keywords: generalized Horn implications
zbMATH Keywords: NP-completeness
zbMATH Keywords: PSPACE-completeness
zbMATH Keywords: Horn fragments of linear logic
zbMATH Keywords: complexity of derivability
zbMATH Keywords: Horn programs
MaRDI profile type: Publication
cites work: Computational interpretations of linear logic
cites work: Q4198056
cites work: Linear logic
cites work: Bounded linear logic: A modular approach to polynomial-time computability
cites work: Efficient program synthesis: Semantics, logic, complexity
cites work: Intuitionistic propositional logic is polynomial-space complete
cites work: Q4495851
description: scientific article; zbMATH DE number 683707