论文标题
无限和圆形证明的弹跳线
Bouncing threads for infinitary and circular proofs
论文作者
论文摘要
我们概括了具有固定点的乘法添加线性逻辑的无限证明系统的有效性标准。我们的标准旨在考虑公理和切割。我们表明它是合理的，并享受了剪切式的属性。我们最终研究了其可定性性能，并证明它通常是不可决定的，但在某些限制下变得可决定。
We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut elimination property. We finally study its decidability properties, and prove that it is undecidable in general but becomes decidable under some restrictions.
