Circular Proofs for G\"odel-L\"ob Logic
  We present a sequent-style proof system for provability logic GL that admits so-called circular proofs. For these proofs, the graph underlying a proof is not a finite tree but is allowed to contain cycles. As an application, we establish Lindon interpolation for GL syntactically. 
Daniyar Shamkanov
math.LO cs.LO