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 progressive 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.

翻译：我们研究基于简洁逻辑的非良基证明系统，这是线性逻辑的一个较弱的变体，其中指数模态 ! 被解释为有限数据上流结构的构造子。逻辑一致性通过在全局层面应用标准的进展准则得以维持。我们提出了一种基于有限近似的无穷切割消去版本，并证明在进展准则存在的情况下，该过程在其极限处能够返回良定义的（well-defined）非良基证明。此外，我们证明了切割消去保持进展准则以及内化证明论统一性程度的多种正则性条件。最后，我们基于关系模型为该系统提供了指称语义。