The complexity of Horn fragments of linear logic (Q1337693)

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.