Logica Universalis 8 (2):141-164 (2014)

Katalin Bimbo
University of Alberta
The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of ${T_\to}$. Here we describe an algorithm to extract an inhabitant from a sequent calculus proof—without translating the proof into another proof system.
Keywords Ackermann constants  combinators  decidability  inhabitation  relevance logics  sequent calculi  structurally free logics  ticket entailment  type assignment systems
Categories (categorize this paper)
DOI 10.1007/s11787-014-0099-z
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,856
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Completeness Theorem in Modal Logic.Saul A. Kripke - 1959 - Journal of Symbolic Logic 24 (1):1-14.
The Undecidability of Entailment and Relevant Implication.Alasdair Urquhart - 1984 - Journal of Symbolic Logic 49 (4):1059-1073.
Combinators and Structurally Free Logic.J. Dunn & R. Meyer - 1997 - Logic Journal of the IGPL 5 (4):505-537.
Normalization as a Homomorphic Image of Cut-Elimination.Garrel Pottinger - 1977 - Annals of Mathematical Logic 12 (3):323.

View all 7 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

New Consecution Calculi for $R^{T}_{\To}$.Katalin Bimbó & J. Michael Dunn - 2012 - Notre Dame Journal of Formal Logic 53 (4):491-509.
Types of I -Free Hereditary Right Maximal Terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5/6):607 - 620.
LEt ® , LR °[^( ~ )], LK and Cutfree Proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
Dual Gaggle Semantics for Entailment.Katalin Bimbó - 2009 - Notre Dame Journal of Formal Logic 50 (1):23-41.
The Power of Belnap: Sequent Systems for SIXTEEN ₃. [REVIEW]Heinrich Wansing - 2010 - Journal of Philosophical Logic 39 (4):369 - 393.
Sequent Calculi for Some Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2009 - Review of Symbolic Logic 2 (2):374-395.
Cuts, Gluts and Gaps.Vincent Degauquier - 2012 - Logique Et Analyse 55 (218):229-240.
A Survey of Nonstandard Sequent Calculi.Andrzej Indrzejczak - 2014 - Studia Logica 102 (6):1295-1322.
Labeled Sequent Calculi for Modal Logics and Implicit Contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.


Added to PP index

Total views
26 ( #396,702 of 2,401,764 )

Recent downloads (6 months)
6 ( #126,902 of 2,401,764 )

How can I increase my downloads?


My notes