A formal framework for specifying sequent calculus proof systems
From MaRDI portal
Publication:1944778
DOI10.1016/j.tcs.2012.12.008zbMath1259.03077OpenAlexW2033813295WikidataQ57850790 ScholiaQ57850790MaRDI QIDQ1944778
Elaine Pimentel, Dale A. Miller
Publication date: 27 March 2013
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2012.12.008
Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items (18)
A linear logic framework for multimodal logics ⋮ A formally verified cut-elimination procedure for linear nested sequents for tense logic ⋮ An Analytic Propositional Proof System on Graphs ⋮ A pure view of ecumenical modalities ⋮ An Evaluation-Driven Decision Procedure for G3i ⋮ Compositional meaning in logic ⋮ Unnamed Item ⋮ A framework for linear authorization logics ⋮ A fresh view of linear logic as a logical framework ⋮ Focused proof-search in the logic of bunched implications ⋮ Multi-focused proofs with different polarity assignments ⋮ Hybrid and subexponential linear logics ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Hybrid linear logic, revisited ⋮ Mechanizing focused linear logic in Coq ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ A focused linear logical framework and its application to metatheory of object logics
Uses Software
This page was built for publication: A formal framework for specifying sequent calculus proof systems
