Cut-Elimination for Provability Logic by Terminating Proof-Search
| Autor: | Gore, Rajeev, Ramanayake, Revantha, Shillito, Ian, Das, Anupam, Negri, S. |
|---|---|
| Přispěvatelé: | Fundamental Computing Science |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021., 299-313 STARTPAGE=299;ENDPAGE=313;TITLE=Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science ISBN: 9783030860585 TABLEAUX |
| ISSN: | 0302-9743 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|