arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2005.08257cs.LO
收藏

无穷大和循环证明的跳跃线程

Bouncing threads for infinitary and circular proofs

David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin

摘要:

推广了乘加线性逻辑不动点无穷证明系统的有效性准则。我们的标准是为了考虑到公理和削减。我们证明了它是合理的,并享有削减消除性质。最后,我们研究了它的可判定性,证明了它在一般情况下是不可判定的,但在某些限制条件下是可判定的。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑