×

zbMATH — the first resource for mathematics

The complexity of Horn fragments of linear logic. (English) Zbl 0812.03007
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.

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
PDF BibTeX Cite
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.