Implicational relevance logic is 2-\textsc{ExpTime}-complete

DOI10.1017/JSL.2015.7MaRDI QIDQ3188334zbMATH OpenOpenAlexFDO

Authors Sylvain Schmitz

Publication date 19 August 2016

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.0705

zbMATH Keywords

complexityrelevance logicfocusing proofsbranching vector addition systems (BVASS)

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Abstract: We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems.

Recommendations

• The complexity of decision procedures in relevance logic II
• Proof finding algorithms for implicational logics
• An \(O(n \log n)\)-space decision procedure for the relevance logic \(B^+\)
• Relevance logic: problems open and closed
• Structural completeness in relevance logics

Cites work

• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• Decision problems for propositional linear logic
• Intuitionistic propositional logic is polynomial-space complete
• Logic Programming with Focusing Proofs in Linear Logic
• Minimalist grammars in the light of logic
• The complexity of the word problems for commutative semigroups and polynomial ideals
• The covering and boundedness problems for branching vector addition systems
• Ticket Entailment is decidable

Cited in

(5)

• A Logical Autobiography
• On the decision problem for MELL
• scientific article; zbMATH DE number 7204434 (Why is no real title available?)
• Constructive decision via redundancy-free proof-search
• There exist exactly two maximal strictly relevant extensions of the relevant logic R

This page was built for publication: Implicational relevance logic is 2-\textsc{ExpTime}-complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3188334)