@article(Berardi:2019aa,
 author       = {S. Berardi and M. Tatsuta},
 year         = {2019},
 title        = {Classical System of {M}artin-{L}of's Inductive Definitions is not Equivalent to Cyclic Proofs},
 journal      = {Logical Methods in Computer Science},
 volume       = {15},
 number       = {3},
 doi          = {10.23638/LMCS-15(3:10)2019},
)
@inproceedings(Brotherston:2005qy,
 author       = {J. Brotherston},
 year         = {2005},
 title        = {Cyclic Proofs for First-Order Logic with Inductive Definitions},
 booktitle    = {Proceedings of {TABLEAUX-14}},
 series       = {LNAI},
 volume       = {3702},
 publisher    = {Springer-Verlag},
 pages        = {78--92},
 doi          = {10.1007/11554554_8},
)
@phdthesis(Brotherston:2006uy,
 author       = {J. Brotherston},
 year         = {2006},
 title        = {Sequent Calculus Proof Systems for Inductive Definitions},
 school       = {University of Edinburgh},
)
@inproceedings(Brotherston:2012fk,
 author       = {J. Brotherston and N. Gorogiannis and R. L. Petersen},
 year         = {2012},
 title        = {A Generic Cyclic Theorem Prover},
 booktitle    = {APLAS-10 (10th Asian Symposium on Programming Languages and Systems)},
 series       = {LNCS},
 volume       = {7705},
 publisher    = {Springer},
 pages        = {350--367},
 doi          = {10.1007/978-3-642-35182-2_25},
)
@article(Brotherston:2011fk,
 author       = {J. Brotherston and A. Simpson},
 year         = {2011},
 title        = {Sequent calculi for induction and infinite descent},
 journal      = {Journal of Logic and Computation},
 volume       = {21},
 number       = {6},
 pages        = {1177--1216},
 doi          = {10.1093/logcom/exq052},
)
@article(Dershowitz:2007bf,
 author       = {N. Dershowitz and G. Moser},
 year         = {2007},
 title        = {The {H}ydra Battle Revisited},
 journal      = {Rewriting, Computation and Proof},
 pages        = {1--27},
 doi          = {10.1007/978-3-540-73147-4\_1},
)
@article(Gentzen:1935fk,
 author       = {G. Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en. {I}},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@techreport(Michel:1988aa,
 author       = {M. Michel},
 year         = {1988},
 title        = {Complementation is more difficult with automata on infinite words},
 type         = {Technical Report},
 institution  = {CNET},
)
@inproceedings(Stratulat:2017ac,
 author       = {S. Stratulat},
 year         = {2017},
 title        = {Cyclic Proofs with Ordering Constraints},
 editor       = {R. A. Schmidt and C. Nalon},
 booktitle    = {TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods)},
 series       = {LNAI},
 volume       = {10501},
 publisher    = {Springer},
 pages        = {311--327},
 doi          = {10.1007/978-3-319-66902-1_19},
)
@inproceedings(Stratulat:2018ab,
 author       = {S. Stratulat},
 year         = {2018},
 title        = {Validating Back-links of {FOL}$_{\unhbox\voidb@x \hbox{\uppercase{{ID}}}}$ Cyclic Pre-proofs},
 editor       = {S. Berardi and S. van Bakel},
 booktitle    = {CL\&C'18 (Seventh International Workshop on Classical Logic and Computation)},
 series       = {{EPTCS}},
 volume       = {281},
 pages        = {39--53},
 doi          = {10.4204/EPTCS.281.4},
)