The complexity of Horn fragments of linear logic.

*(English)*Zbl 0812.03007Complexity 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.

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.

Reviewer: M.K.Val’ev (Moskva)

##### MSC:

03B20 | Subsystems of classical logic (including intuitionistic logic) |

03D15 | Complexity of computation (including implicit computational complexity) |

68Q25 | Analysis of algorithms and problem complexity |

03B25 | Decidability of theories and sets of sentences |

##### Keywords:

generalized Horn implications; NP-completeness; PSPACE-completeness; Horn fragments of linear logic; complexity of derivability; Horn programs
PDF
BibTeX
Cite

\textit{M. I. Kanovich}, Ann. Pure Appl. Logic 69, No. 2--3, 195--241 (1994; Zbl 0812.03007)

Full Text:
DOI

##### References:

[1] | Abramsky, S., Computational interpretations of linear logic, Theoret. comput. sci., 111, 3-57, (1993), Special Issue on the 1990 Workshop on Math. Found. Prog. Semantics · Zbl 0791.03003 |

[2] | Asperti, A.; Ferrari, G.-L.; Gorrieri, R., Implicative formulae in the ‘proofs as computations’ analogy, Proceedings of the 17th ACM symp. on principles of programming languages, 59-71, (January 1990), San Francisco |

[3] | Garey, M.R.; Johnson, D.S., Computers and intractability: A guide to the theory of NP-completeness, (1979) · Zbl 0411.68039 |

[4] | Girard, J.-Y., Linear logic, Theoret. comput. sci., 50, 1-102, (1987) · Zbl 0625.03037 |

[5] | Girard, J.-Y.; Scedrov, A.; Scott, P.J., Bounded linear logic: a modular approach to polynomial time computability, Theoret. comput. sci., 97, 1-66, (1992) · Zbl 0788.03005 |

[6] | Kanovich, M.I., The multiplicative fragment of linear logic is NP-complete, Technical report X-91-13, (1991), University of Amsterdam, Institute for Language, Logic, and Information |

[7] | Kanovich, M.I., The Horn fragment of linear logic is NP-complete, Technical report X-91-14, (1991), University of Amsterdam, Institute for Language, Logic, and Information |

[8] | Kanovich, M.I., Efficient program synthesis: semantics, logic, complexity, (), 615-632, Theoretical Aspects of Computer Software, TACS’91, Japan, Sendai |

[9] | Kanovich, M.I., Fast theorem proving in intuitionistic propositional logic, Technical report CS-R9157, (1991), Centre for Mathematics and Computer Science, Computer Science/Department of Software Technology Amsterdam |

[10] | Kanovich, M.I., Horn programming in linear logic is NP-complete, Proceeding of the 7th annual IEEE symposium on logic in computer science, 200-210, (June 1992), Santa Cruz |

[11] | Lincoln, P.; Mitchell, J.; Scedrov, A.; Shankar, N.; Lincoln, P.; Mitchell, J.; Scedrov, A.; Shankar, N., Decision problems for propositional linear logic, Ann. pure appl. logic, Preliminary report in Proceedings of the 31st IEEE symp. on foundations of computer science, 56, 662-671, (1990) |

[12] | Lincoln, P.; Scedrov, A.; Shankar, N.; Lincoln, P.; Scedrov, A.; Shankar, N., Linearizing intuitionistic implication, Ann. pure appl. logic, Preliminary report in Proceedings of the 6th annual IEEE symposium on logic in computer science, 60, 51-62, (1991), Amsterdam |

[13] | Lincoln, P.; Winkler, T., Constant multiplicative linear logic is NP-complete, Draft, (1992) |

[14] | Pratt, V.R., Event spaces and their linear logic, (), 1-23, Workshops in Computing |

[15] | Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoret. comput. sci., 9, 67-72, (1979) · Zbl 0411.03049 |

[16] | Troelstra, A.S., Lectures on linear logic, CSLI lecture notes no. 29, (1992), Stanford University, Center for the Study of Language and Information · Zbl 0942.03535 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.