Local validity for circular proofs in linear logic with fixed points

DOI10.4230/LIPICS.CSL.2018.35MaRDI QIDQ5079760zbMATH OpenFDO

Authors Rémi Nollet, Alexis Saurin, Christine Tasson

Publication date 28 May 2022

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2018.35

zbMATH Keywords

fixed pointslinear logicinductioncoinductionsequent calculusfinitizationinfproof-searchcircular proofsnon-wellfounded proofsmuMALL

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• Decision problems for linear logic with least and greatest fixed points
• Circular proofs as session-typed processes: a local validity condition
• scientific article; zbMATH DE number 2087442

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 7297836 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• A Proof System for the Linear Time μ-Calculus
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Constructive completeness for the linear-time -calculus
• Cyclic arithmetic is equivalent to Peano arithmetic
• Equivalence of inductive definitions and cyclic proofs under arithmetic
• Infinitary proof theory: the multiplicative additive case
• Least and Greatest Fixpoints in Game Semantics
• Linear logic
• On modal mu-calculus and Büchi tree automata
• On the Proof Theory of Regular Fixed Points
• Results on the propositional \(\mu\)-calculus
• Sequent calculi for induction and infinite descent
• The size-change principle for program termination
• The structure of multiplicatives
• Towards completeness via proof search in the linear time -calculus: the case of Büchi inclusions

Cited in

(6)

• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Circular proofs as session-typed processes: a local validity condition
• Fragments of arithmetic and cyclic proofs
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• Decision problems for linear logic with least and greatest fixed points

Describes a project that uses

Uses Software

• Cyclist

This page was built for publication: Local validity for circular proofs in linear logic with fixed points

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