A formally verified cut-elimination procedure for linear nested sequents for tense logic
From MaRDI portal
Publication:2142082
DOI10.1007/978-3-030-86059-2_17OpenAlexW3198628855MaRDI QIDQ2142082
Caitlin D'Abrera, Rajeev Goré, Jeremy E. Dawson
Publication date: 25 May 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_17
tense logiccut-eliminationprogram synthesisCoqextractionformalised proof theorylinear nested sequent calculus
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proof analysis in modal logic
- Cut-free sequent calculi for some tense logics
- Display logic
- A formal framework for specifying sequent calculus proof systems
- Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
- A fresh view of linear logic as a logical framework
- Mechanizing focused linear logic in Coq
- Formalized meta-theory of sequent calculi for linear logics
- Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
- Formalizing Cut Elimination of Coalgebraic Logics in Coq
- Structural Focalization
- From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
- Constructive decision via redundancy-free proof-search
This page was built for publication: A formally verified cut-elimination procedure for linear nested sequents for tense logic