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 QIDQ6541152FDO

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

• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• scientific article; zbMATH DE number 2087442 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 7533344 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• A Proof System for the Linear Time μ-Calculus
• A finite model theorem for the propositional \(\mu\)-calculus
• A new deconstructive logic: linear logic
• Automated cyclic entailment proofs in separation logic
• Categorical semantics of linear logic
• Coinductive foundations of infinitary rewriting and infinitary equational logic
• Constructive completeness for the linear-time \(\mu \)-calculus
• Infinitary proof theory: the multiplicative additive case
• Linear logic
• On closure ordinals for the modal \(\mu\)-calculus
• Results on the propositional \(\mu\)-calculus
• Sequent calculi for induction and infinite descent
• Syntactic cut-elimination for a fragment of the modal mu-calculus

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)