  Infinitary and cyclic proof systems are proof systems for logical formulas
with fixed-point operators or inductive definitions. A cyclic proof system is a
restriction of the corresponding infinitary proof system. Hence, these proof
systems are generally not the same, as in the cyclic system may be weaker than
the infinitary system. For several logics, the infinitary proof systems are
shown to be cut-free complete. However, cyclic proof systems are characterized
with many unknown problems on the (cut-free) completeness or the
cut-elimination property. In this study, we show that the provability of
infinitary and cyclic proof systems are the same for some propositional logics
with fixed-point operators or inductive definitions and that the cyclic proof
systems are cut-free complete.
