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

branching vector addition systems (BVASS)complexityfocusing proofsrelevance logic

Mathematics Subject Classification ID

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

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 n)-space decision procedure for the relevance logic B^+
• Relevance logic: problems open and closed
• Structural completeness in relevance logics

Cites work

• Decision problems for propositional linear logic
• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• 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

(6)

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

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)