A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates

Yukihiro Oda, Daisuke Kimura

The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for suc…