Issues in Machine-Checking the Decidability of Implicational Ticket Entailment

摘要

The decidability of the implicational fragment T→ of the relevance logic of ticket entailment was recently claimed independently by Bimbo and Dunn, and Padovani. We present a mechanised formalisation, in Isabelle/HOL, of the various proof-theoretical results due to Bimbo and Dunn that underpin their claim. We also discuss the issues that stymied our attempt to verify their proof of decidability.