@inproceedings{deecd2d315604a2caf42ecf349a5cbe4,

title = "Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq",

abstract = "Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximum height of regress trees in an auxiliary calculus called RGL. Tautology elimination is established rather than direct cut-admissibility, and at some points the input derivation appears to be ignored in favour of a derivation obtained by backward proof-search. By formalising the GLS calculus and the proofs in Coq, we show that: (1) the use of the novel measure is problematic under the usual interpretation of the Gentzen comma as set union, and a multiset-based sequent calculus provides a more natural formulation; (2) the detour through tautology elimination is unnecessary; and (3) we can use the same induction argument without regress trees to obtain a direct proof of cut-admissibility that is faithful to the input derivation.",

author = "Rajeev Gore and Revantha Ramanayake and Ian Shillito",

year = "2021",

doi = "10.1007/978-3-030-86059-2_18",

language = "English",

isbn = "978-3-030-86058-5",

series = " Lecture Notes in Computer Science",

publisher = "Springer",

pages = "299--313",

editor = "Das, {Anupam } and {Negri }, S.",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021.",

note = "30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods : TABLEAUX 2021: Automated Reasoning with Analytic Tableaux and Related Methods ; Conference date: 06-09-2021 Through 09-09-2021",

}