Cut elimination for propositional cyclic proof systems with fixed-point operators

Hiromasa Hori, Koji Nakazawa, Makoto Tatsuta

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 corres…