×

zbMATH — the first resource for mathematics

Implicational relevance logic is 2-ExpTime-complete. (English) Zbl 1370.03029
This paper establishes that provability in the pure implication fragment \(\mathbf{R}_\to\) of the relevance logic R is 2-ExpTime-complete. This draws crucially on the result of S. Demri et al. [J. Comput. Syst. Sci. 79, No. 1, 23–38 (2013; Zbl 1260.68264)] that the covering and boundedness problems for branching vector addition systems with states (BVASS) are themselves 2-ExpTime-complete. The author shows that expansive BVASSs can simulate proofs in \(\mathbf{R}_\to\), or its sequent formulation \(\mathit{L}\mathbf{R}_\to\), and that their reachability reduces to coverability. This provides a decision procedure for \(\mathbf{R}_\to\) in 2-ExpTime. As BVASS coverability can be reduced to provability in \(\mathbf{R}_\to\), this provides its 2-ExpTime-hardness. The latter result draws on a variant sequent calculus for \(\mathbf{R}_\to\), viz. \(\mathit{F}\mathbf{R}_\to\), for focusing proofs (cf. [J.-M. Andreoli, J. Log. Comput. 2, No. 3, 297–347 (1992; Zbl 0764.03020)] for linear logic).

MSC:
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Methodos, 2 pp 56– (1950)
[2] DOI: 10.1017/S0960129512000412 · Zbl 1280.03014 · doi:10.1017/S0960129512000412
[3] Proceedings of Concur 2013 8052 pp 152– (2013)
[4] DOI: 10.1016/0168-0072(92)90075-B · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B
[5] Proceedings of ASL 1959 24 pp 324– (1959)
[6] Proceedings of ACL 2001 pp 252– (2001)
[7] Combinatory logic, vol. 1 22 (1958)
[8] Handbook of philosophical logic 6 pp 1– (2002)
[9] Kontrolliertes Denken. Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften pp 22– (1951)
[10] ACM Transactions on Programming Languages and Systems 35 (2013)
[11] DOI: 10.1016/j.jcss.2012.04.002 · Zbl 1260.68264 · doi:10.1016/j.jcss.2012.04.002
[12] Journal of the ACM 56 pp 1– (2009)
[13] DOI: 10.1093/logcom/2.3.297 · Zbl 0764.03020 · doi:10.1093/logcom/2.3.297
[14] Entailment: The logic of relevance and necessity I (1975) · Zbl 0323.02030
[15] Discrete Mathematics and Theoretical Computer Science 7 pp 217– (2005)
[16] DOI: 10.1007/978-94-009-0681-5_5 · doi:10.1007/978-94-009-0681-5_5
[17] DOI: 10.1016/0304-3975(79)90006-9 · Zbl 0411.03049 · doi:10.1016/0304-3975(79)90006-9
[18] Proceedings of ACL 2010 pp 514– (2010)
[19] DOI: 10.1007/978-3-642-21490-5_5 · Zbl 1339.03026 · doi:10.1007/978-3-642-21490-5_5
[20] Proceedings of CSL ’98 1584 pp 224– (1999)
[21] Proceedings of ACL’94 pp 263– (1994)
[22] DOI: 10.1016/0001-8708(82)90048-2 · Zbl 0506.03007 · doi:10.1016/0001-8708(82)90048-2
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.