A formally verified cut-elimination procedure for linear nested sequents for tense logic
type: Item
instance of: scholarly article
title: A formally verified cut-elimination procedure for linear nested sequents for tense logic
DOI: 10.1007/978-3-030-86059-2_17
author: Caitlin D'Abrera
author: Rajeev Goré
author: Jeremy E. Dawson
publication date: 2022-05-25T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7532522
zbMATH Keywords: formalised proof theory
zbMATH Keywords: cut-elimination
zbMATH Keywords: linear nested sequent calculus
zbMATH Keywords: tense logic
zbMATH Keywords: Coq
zbMATH Keywords: extraction
zbMATH Keywords: program synthesis
describes a project that uses: Coq
describes a project that uses: Haskell
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: 978-3-030-86059-2 17
OpenAlex ID: W3198628855
cites work: Display logic
cites work: Formalized meta-theory of sequent calculi for linear logics
cites work: Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
cites work: From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
cites work: Q4484337
cites work: Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
cites work: Tableau methods for modal and temporal logics
cites work: Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
cites work: Cut-free sequent calculi for some tense logics
cites work: Constructive decision via redundancy-free proof-search
cites work: A formal framework for specifying sequent calculus proof systems
cites work: Proof analysis in modal logic
cites work: A fresh view of linear logic as a logical framework
cites work: Structural Focalization
cites work: Formalizing Cut Elimination of Coalgebraic Logics in Coq
cites work: Q4716271
cites work: Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
cites work: Mechanizing focused linear logic in Coq
description: scientific article