zbMATH — the first resource for mathematics

Disjunction property and complexity of substructural logics. (English) Zbl 1231.03021
Summary: We systematically identify a large class of substructural logics that satisfy the disjunction property (DP), and show that every consistent substructural logic with the DP is PSPACE-hard. Our results are obtained by using algebraic techniques. PSPACE-completeness for many of these logics is furthermore established by proof-theoretic arguments.

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03D15 Complexity of computation (including implicit computational complexity)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI
[1] Aguzzoli, S.; Gerla, B.; Haniková, Z., Complexity issues in basic logic, Soft computing, 9, 919-934, (2005) · Zbl 1093.03010
[2] Bulińska, M., On the complexity of nonassociative lambek calculus with unit, Studia logica, 93, 1-14, (2009) · Zbl 1182.03041
[3] Burris, S.; Sankappanavar, H.P., A course in universal algebra, (1981), Springer · Zbl 0478.08001
[4] Chagrov, A.; Zakharyaschev, M., ()
[5] A. Ciabattoni, N. Galatos, K. Terui, From axioms to analytic rules in nonclassical logics, in: Proceedings of IEEE Symposium on Logic in Computer Science, 2008, pp. 229-240.
[6] A. Ciabattoni, N. Galatos, K. Terui, Algebraic proof theory for substructural logics: cut-elimination and completions (submitted for publication). Available at: http://www.kurims.kyoto-u.ac.jp/ terui/apt.pdf. · Zbl 1245.03026
[7] Ciabattoni, A.; Straßburger, L.; Terui, K., Expanding the realm of systematic proof theory, (), 163-178 · Zbl 1257.03084
[8] Dunn, J.M.; Restall, G., (), 1-128
[9] Feder, T.; Vardi, M.Y., The computational structure of monotone monadic SNP and constraint satisfaction: a study through Datalog and group theory, SIAM journal on computing, 28, 1, 57-104, (1999) · Zbl 0914.68075
[10] Galatos, N.; Jipsen, P.; Kowalski, T.; Ono, H., ()
[11] Galatos, N.; Ono, H., Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL, Studia logica, 83, 1-3, 279-308, (2006) · Zbl 1105.03021
[12] Girard, J.-Y., Linear logic, Theoretical computer science, 50, 1-102, (1987) · Zbl 0625.03037
[13] de Groote, P.; Lamarche, F., Classical non-associative lambek calculus, Studia logica, 71, 355-388, (2002) · Zbl 1032.03014
[14] Hájek, P., ()
[15] Kanazawa, M., Lambek calculus: recognizing power and complexity, ()
[16] M.I. Kanovich, The multiplicative fragment of Linear Logic is NP-complete, Tech. Report X-91-13, University of Amsterdam, Institute for Language, Logic, and Information, 1991.
[17] M.I. Kanovich, Horn fragments of non-commutaive logics with additives are PSPACE-complete, in: 1994 Annual Conference of the European Association for Computer Science Logic, Kazimierz, Poland, 1994.
[18] Lincoln, P., Deciding provability of linear logic formulas, Advances in linear logic, 109-122, (1995) · Zbl 0823.03004
[19] Lincoln, P.; Mitchell, J.; Scedrov, A.; Shankar, N., Decision problems for propositional linear logic, Annals of pure and applied logic, 56, 1-3, 239-311, (1992) · Zbl 0768.03003
[20] O’Hearn, P.W.; Pym, D.J., The logic of bunched implications, Bulletin of symbolic logic, 5, 2, 215-244, (1999) · Zbl 0930.03095
[21] Papadimitriou, C.H., Computational complexity, (1994), Addison-Wesley Publishing Company Reading, MA · Zbl 0557.68033
[22] Restall, Greg, An introduction to substructural logics, (2000), Routledge · Zbl 1028.03018
[23] John C. Reynolds, Separation logic: a logic for shared mutable data structures, in: Proceedings of IEEE Symposium on Logic in Computer Science, 2002, pp. 55-74.
[24] Souma, D., An algebraic approach to the disjunction property of substructural logics, Notre dame journal of formal logic, 48, 4, 489-495, (2007) · Zbl 1137.03012
[25] Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoretical computer science, 9, 1, 67-72, (1979) · Zbl 0411.03049
[26] Švejdar, V., On the polynomial-space completeness of intuitionistic propositional logic, Archive for mathematical logic, 42, 711-716, (2003) · Zbl 1025.03030
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.