Bouncing threads for infinitary and circular proofs
Logic in Computer Science
2020-05-19 v1
Abstract
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.
Cite
@article{arxiv.2005.08257,
title = {Bouncing threads for infinitary and circular proofs},
author = {David Baelde and Amina Doumane and Denis Kuperberg and Alexis Saurin},
journal= {arXiv preprint arXiv:2005.08257},
year = {2020}
}