@inproceedings{004a8837c5a8461f9ba23d56d712a8c2,
title = "Issues in machine-checking the decidability of implicational ticket entailment",
abstract = "The decidability of the implicational fragment T→ of the relevance logic of ticket entailment was recently claimed independently by Bimb{\'o} and Dunn, and Padovani. We present a mechanised formalisation, in Isabelle/HOL, of the various proof-theoretical results due to Bimb{\'o} and Dunn that underpin their claim. We also discuss the issues that stymied our attempt to verify their proof of decidability.",
author = "Dawson, {Jeremy E.} and Rajeev Gor{\'e}",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017 ; Conference date: 25-09-2017 Through 28-09-2017",
year = "2017",
doi = "10.1007/978-3-319-66902-1_21",
language = "English",
isbn = "9783319669014",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "347--363",
editor = "Claudia Nalon and Schmidt, {Renate A.}",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Proceedings",
address = "Germany",
}