PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points

DOI10.1007/978-3-030-29026-9_18zbMath1435.03088OpenAlexW2953665898MaRDI QIDQ2180526

Alexis Saurin, Rémi Nollet, Christine Tasson

Publication date: 14 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-29026-9_18

zbMATH Keywords

complexityfixed pointssequent calculuslinear logicinductionPSPACE-completecoinductioncircular proofsnon-wellfounded proofs\(\mu\mathrm{MLL}\)size-change

Mathematics Subject Classification ID

Structure of proofs (03F07) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (3)

Abstract cyclic proofs ⋮ Kleene star, subexponentials without contraction, and infinite computations ⋮ Non-well-founded deduction for induction and coinduction

Uses Software

• Cyclist

This page was built for publication: PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points