Formalized meta-theory of sequent calculi for substructural logics

DOI10.1016/j.entcs.2017.04.005zbMath1401.03033OpenAlexW2650704808WikidataQ113317596 ScholiaQ113317596MaRDI QIDQ1744443

Xianqiang Yang

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2017.04.005

zbMATH Keywords

cut eliminationsequent calculuslinear logicAbellaformalized proof

Mathematics Subject Classification ID

Related Items (5)

Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ Unnamed Item ⋮ Formal meta-level analysis framework for quantum programming languages ⋮ Mechanizing focused linear logic in Coq

Uses Software

• Abella

Cites Work

• Unnamed Item
• Nominal abstraction
• 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
• Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
• Abella: A System for Reasoning about Relational Specifications

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