Formalized meta-theory of sequent calculi for linear logics

DOI10.1016/j.tcs.2019.02.023zbMath1425.03007OpenAlexW2918427073WikidataQ128293074 ScholiaQ128293074MaRDI QIDQ2424887

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

sequent calculuslinear logicproof theorylogic programmingmechanized meta-theory

Mathematics Subject Classification ID

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

Related Items

A linear logic framework for multimodal logics, A formally verified cut-elimination procedure for linear nested sequents for tense logic, A focused linear logical framework and its application to metatheory of object logics

Uses Software

• Abella

Cites Work

• Unnamed Item
• Nominal abstraction
• Formalized meta-theory of sequent calculi for substructural logics
• A note on full intuitionistic linear logic
• A two-level logic approach to reasoning about computations
• Formalizing Cut Elimination of Coalgebraic Logics in Coq
• VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED
• Structural Focalization
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents
• Logic Programming with Focusing Proofs in Linear Logic
• Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
• Parametric higher-order abstract syntax for mechanized semantics
• Abella: A System for Reasoning about Relational Specifications