A formally verified cut-elimination procedure for linear nested sequents for tense logic

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

zbMATH Keywords

tense logiccut-eliminationprogram synthesisCoqextractionformalised proof theorylinear nested sequent calculus

Mathematics Subject Classification ID

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

Related Items

A linear logic framework for multimodal logics

Uses Software

• Coq
• Haskell
• GitHub

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