Formalized meta-theory of sequent calculi for linear logics

DOI10.1016/J.TCS.2019.02.023MaRDI QIDQ2424887zbMATH OpenOpenAlexWikidataFDO

Authors Yanyan Li

Publication date 25 June 2019

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2019.02.023

zbMATH Keywords

proof theorylinear logicsequent calculuslogic programmingmechanized meta-theory

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Mechanization of proofs and logical operations (03B35) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Formalized meta-theory of sequent calculi for substructural logics
• scientific article; zbMATH DE number 1950250
• scientific article; zbMATH DE number 2152687
• A framework for proof systems
• Focusing in Linear Meta-logic

Cites work

• A note on full intuitionistic linear logic
• A two-level logic approach to reasoning about computations
• Abella: a system for reasoning about relational specifications
• Formalized meta-theory of sequent calculi for substructural logics
• Formalizing cut elimination of coalgebraic logics in Coq
• Generic methods for formalising sequent calculi applied to provability logic
• Label-free modular systems for classical and intuitionistic modal logics
• Logic Programming with Focusing Proofs in Linear Logic
• Nominal abstraction
• Parametric higher-order abstract syntax for mechanized semantics
• Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• Structural focalization
• Valentini's cut-elimination for provability logic resolved

Cited in

(12)

• Sequent Calculi for Intuitionistic Linear Logic with Strong Negation
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A linear logic framework for multimodal logics
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• A linear algebra approach to linear metatheory
• From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
• A focused linear logical framework and its application to metatheory of object logics
• Computer Science Logic
• Formalization of linear space theory in the higher-order logic proving system
• Formalized meta-theory of sequent calculi for substructural logics
• A simplified account of the metatheory of linear LF
• Proving structural properties of sequent systems in rewriting logic

Describes a project that uses

Uses Software

• Abella

This page was built for publication: Formalized meta-theory of sequent calculi for linear logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2424887)