2026-07-25T05:50:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19651 2024-03-06T11:04:33Z ddc:004 open_access

Infinitary Cut-Elimination via Finite Approximations Acclavio, Matteo Curzi, Gianluca Guerrieri, Giulio cut-elimination non-wellfounded proofs parsimonious logic linear logic proof theory approximation sequent calculus non-uniform proofs We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matteo Acclavio and Gianluca Curzi and Giulio Guerrieri 2024 Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2024.8 urn:nbn:de:0030-drops-196510 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8 eng https://creativecommons.org/licenses/by/4.0/legalcode