On the decidability of implicational ticket entailment

DOI10.2178/JSL.7801150MaRDI QIDQ4916555zbMATH OpenOpenAlexFDO

Authors Katalin Bimbó, J. Michael Dunn

Publication date 23 April 2013

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

Full work available at URL https://projecteuclid.org/euclid.jsl/1358951110

zbMATH Keywords

decidabilityrelevance logicssequent calculiticket entailmentnon-associativityAckermann constantsadmissibility of cut

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Decidability of theories and sets of sentences (03B25) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• New consecution calculi for \(R^{t}_{\to}\)
• Ticket Entailment is decidable
• Issues in machine-checking the decidability of implicational ticket entailment
• \(TW_+\) and \(RW_+\) are decidable
• The complexity of decision procedures in relevance logic II

Cites work

• scientific article; zbMATH DE number 3261581 (Why is no real title available?)
• Admissibility of cut in LC with fixed point combinator
• Combinators and structurally free logic
• Combinatory logic. Pure, applied and typed
• Logic, meaning and computation. Essays in memory of Alonzo Church
• New consecution calculi for \(R^{t}_{\to}\)
• Types of I-free hereditary right maximal terms
• \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs

Cited in

(17)

• New consecution calculi for \(R^{t}_{\to}\)
• Completeness and conservative extension results for some Boolean relevant logics
• Issues in machine-checking the decidability of implicational ticket entailment
• On the decidability of certain semi-lattice based modal logics
• Types of I-free hereditary right maximal terms
• Larisa Maksimova’s Early Contributions to Relevance Logic
• An alternative Gentzenisation of \(\mathsf{RW}_+^\circ\)
• Constructive decision via redundancy-free proof-search
• IN MEMORIAM: J. MICHAEL DUNN, 1941–2021
• scientific article; zbMATH DE number 2015405 (Why is no real title available?)
• Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
• The one-variable fragment of \(\mathrm T_\to\)
• Current trends in substructural logics
• scientific article; zbMATH DE number 2024615 (Why is no real title available?)
• Ticket Entailment is decidable
• The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
• The decidability of the intensional fragment of classical linear logic

This page was built for publication: On the decidability of implicational ticket entailment

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