Hostname: page-component-5cf477f64f-r2nwp Total loading time: 0 Render date: 2025-04-08T07:25:41.962Z Has data issue: false hasContentIssue false
  • English
  • Français

Ticket Entailment is decidable

Published online by Cambridge University Press:  09 July 2012

VINCENT PADOVANI
VINCENT PADOVANI*
Affiliation:
Equipe Preuves, Programmes et Systèmes, Université Paris VII – Denis Diderot, Case 7014, 75205 PARIS Cedex 13, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We prove the decidability of the logic T→ of Ticket Entailment. This issue was first raised by Anderson and Belnap within the framework of relevance logic, and is equivalent to the question of the decidability of type inhabitation in simply typed combinatory logic with the partial basis BB′IW. We solve the equivalent problem of type inhabitation for the restriction of simply typed lambda calculus to hereditarily right-maximal terms.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Issue 3 , June 2013 , pp. 568 - 607
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Anderson, A. R. (1960) Entailment shorn of modality. Journal of Symbolic Logic 25 (4)388.Google Scholar
Anderson, A. R. and Belnap, N. D. Jr (1975) Entailment: The Logic of Relevance and Necessity, Volume 1, Princeton University Press.Google Scholar
Anderson, A. R., Belnap, N. D. Jr and Dunn, J. M. (1990) Entailment: The Logic of Relevance and Necessity, Volume 2, Princeton University Press.Google Scholar
Barendregt, H. (1984) The Lambda Calculus: Its Syntax and Semantics (Revised edition), Studies in Logic and the Foundations of Mathematics 103, North Holland.Google Scholar
Barwise, J. (ed.) (1977) Handbook of Mathematical Logic, Studies in Logic and Foundations of Mathematics, North-Holland.Google Scholar
Bezem, M., Klop, J. W. and de Vrijer, R. (eds.)† (2003) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press.Google Scholar
Bimbó, K. (2005) Types of I-free hereditary right maximal terms. Journal of Philosophical Logic 34 (5-6)607–620.CrossRefGoogle Scholar
Broda, S., Damas, L., Finger, M. and Silva e Silva, P. S. (2004) The decidability of a fragment of BB′IW-logic. Theoretical Computer Science 318 (3)373–408.CrossRefGoogle Scholar
Bunder, M. W. (1996) Lambda Terms Definable as Combinators. Theoretical Computer Science 169 (1)3–21.CrossRefGoogle Scholar
Higman, G. (1952) Ordering by divisibility in abstract algebra. Proceedings of the London Mathematical Society 3 (2)326–336.CrossRefGoogle Scholar
Kripke, S. (1959) The problem of entailment. Journal of Symbolic Logic 24 (4)324.Google Scholar
Krivine, J.-L. (1993) Lambda-calculus, types and models, Masson.Google Scholar
Kruskal, J. B. (1972) The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A 13 (3)297–305.CrossRefGoogle Scholar
Melliès, P.-A. (1998) On a duality between Kruskal and Dershowitz theorems. In: Larsen, K. G, Skyum, S. and Winskel, G. (eds.) ICALP. Springer-Verlag Lecture Notes in Computer Science 1443 518–529.CrossRefGoogle Scholar
Trigg, P., Hindley, J. R. and Bunder, M. W. (1994) Combinatory abstraction using B, B′ and friends. Theoretical Computer Science 135 (2)405–422.CrossRefGoogle Scholar
Urquhart, A (1984) The undecidability of entailment and relevant implication. Journal of Symbolic Logic 49 (4)1059–1073.CrossRefGoogle Scholar