Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq

DOI10.1007/978-3-030-86059-2_18OpenAlexW3197466636MaRDI QIDQ2142084

Revantha Ramanayake, Rajeev Goré, Ian Shillito

Publication date: 25 May 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_18

zbMATH Keywords

proof theoryprovability logicinteractive theorem provingcut admissibility

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Cut elimination by unthreading

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Cut elimination for GLS using the terminability of its regress process
• The modal logic of provability: cut-elimination
• On some proof theoretical properties of the modal logic GL
• Proof analysis in modal logic
• The modal logic of provability. The sequential approach
• Provability interpretations of modal logic
• Cut-elimination for weak Grzegorczyk logic Go
• Proofs and countermodels in non-classical logics
• Cut elimination for the weak modal Grzegorczyk logic via non-well-founded proofs
• VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED
• Tautology Elimination, Cut Elimination, and S5
• Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

This page was built for publication: Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq