A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points

DOI10.1007/978-3-031-43513-3_12MaRDI QIDQ6541152FDOQ6541152

Authors: Alexis Saurin 

Publication date: 17 May 2024

zbMATH Keywords

cut elimination\(\mu \)-calculusnon-wellfounded proofs\textsf{LL}

Mathematics Subject Classification ID

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

Cites Work

• Categorical semantics of linear logic
• Linear logic
• A finite model theorem for the propositional \(\mu\)-calculus
• Results on the propositional \(\mu\)-calculus
• Title not available (Why is that?)
• Syntactic cut-elimination for a fragment of the modal mu-calculus
• Sequent calculi for induction and infinite descent
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new deconstructive logic: linear logic
• Least and Greatest Fixed Points in Linear Logic
• A Proof System for the Linear Time μ-Calculus
• On closure ordinals for the modal \(\mu\)-calculus
• Constructive completeness for the linear-time \(\mu \)-calculus
• Title not available (Why is that?)
• Automated cyclic entailment proofs in separation logic
• Infinitary proof theory: the multiplicative additive case
• Title not available (Why is that?)
• Coinductive foundations of infinitary rewriting and infinitary equational logic

This page was built for publication: A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points

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