Extracting BB'IW inhabitants of simple types from proofs in the sequent calculus LT_^t for implicational ticket entailment

DOI10.1007/S11787-014-0099-ZzbMATH Open1344.03028OpenAlexW2135096857MaRDI QIDQ2254561FDOQ2254561

Authors: Katalin Bimbó, J. Michael Dunn 

Publication date: 5 February 2015

Published in: Logica Universalis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11787-014-0099-z

Recommendations

• Ticket Entailment is decidable
• Types of I-free hereditary right maximal terms
• Inhabitants of intuitionistic implicational theorems
• On the decidability of implicational ticket entailment
• Bounded combinatory logic

zbMATH Keywords

decidabilityrelevance logicssequent calculitype assignment systemsinhabitationticket entailmentcombinatorsAckermann constantsstructurally free logics

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40)

Cites Work

• Combinatory logic. Pure, applied and typed
• Four variables suffice
• The undecidability of entailment and relevant implication
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinators and structurally free logic
• On the decidability of implicational ticket entailment
• Ticket Entailment is decidable
• Title not available (Why is that?)
• New consecution calculi for \(R^{t}_{\to}\)
• Combinatory logic. With two sections by William Craig.
• Lectures on the Curry-Howard isomorphism
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Normalization as a homomorphic image of cut-elimination
• Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Types of I-free hereditary right maximal terms
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Completeness of the normal typed fragment of the \(\lambda\)-system \(U\)
• Title not available (Why is that?)

Cited In (3)

• Current trends in substructural logics
• New consecution calculi for \(R^{t}_{\to}\)
• Inhabitants of intuitionistic implicational theorems

This page was built for publication: Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment

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