Details

Autor(en) / Beteiligte

• D’Abrera, Caitlin
• Dawson, Jeremy
• Goré, Rajeev

Titel

A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic

Ist Teil von

• Automated Reasoning with Analytic Tableaux and Related Methods, p.281-298

Ort / Verlag

Cham: Springer International Publishing

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• We port Dawson and Goré’s general framework of deep embeddings of derivability from Isabelle to Coq. By using lists instead of multisets to encode sequents, we enable the encoding of genuinely substructural logics in which some combination of exchange, weakening and contraction are not admissible. We then show how to extend the framework to encode the linear nested sequent calculus LNSKt\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {LNS}_\mathsf {Kt}$$\end{document} of Goré and Lellmann for the tense logic Kt\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {Kt}$$\end{document} and prove cut-elimination and all required proof-theoretic theorems in Coq, based on their pen-and-paper proofs. Finally, we extract the proof of the cut-elimination theorem to obtain a formally verified Haskell program that produces cut-free derivations from those with cut. We believe it is the first published formally verified computer program for eliminating cuts in any proof calculus.