@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",
}