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

Rajeev Gore, Revantha Ramanayake, Ian Shillito*

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

14 Citaten (Scopus)

Samenvatting

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.
Originele taal-2English
TitelAutomated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021.
RedacteurenAnupam Das, S. Negri
Plaats van productieCham
UitgeverijSpringer
Pagina's299-313
Aantal pagina's14
ISBN van elektronische versie978-3-030-86059-2
ISBN van geprinte versie978-3-030-86058-5
DOI's
StatusPublished - 2021
Evenement30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021: Automated Reasoning with Analytic Tableaux and Related Methods - Birmingham, United Kingdom
Duur: 6-sep-20219-sep-2021

Publicatie series

Naam Lecture Notes in Computer Science
UitgeverijSpringer
Volume12842
ISSN van geprinte versie0302-9743
NaamLecture Notes in Artificial Intelligence
UitgeverijSpringer
Volume12842
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349

Conference

Conference30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Land/RegioUnited Kingdom
StadBirmingham
Periode06/09/202109/09/2021

Citeer dit