Daniyar Shamkanov proved that three distinct systems of sequent calculi for GL are equivalent. These systems consist in one with finite proofs, another with ill-founded proofs and the last one with cyclic proofs. The main tool used for proving the equivalence is corecursion. In this project, we prove the equivalence between a finitary sequent calculus for iGL and a cyclic calculus, using also coinductive methods.

翻译：摘要：Daniyar Shamkanov 证明了GL的三个不同序列演算系统是等价的。这些系统包括一个有限证明系统、一个无基证明系统以及一个循环证明系统。证明等价性的主要工具是余递归。在本项目中，我们同样使用共归纳方法，证明了iGL的有限序列演算与循环演算之间的等价性。