S. Berardi & M. Tatsuta (2019):
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs.
Logical Methods in Computer Science 15(3),
doi:10.23638/LMCS-15(3:10)2019.
J. Brotherston (2005):
Cyclic Proofs for First-Order Logic with Inductive Definitions.
In: Proceedings of TABLEAUX-14,
LNAI 3702.
Springer-Verlag,
pp. 78–92,
doi:10.1007/11554554_8.
J. Brotherston (2006):
Sequent Calculus Proof Systems for Inductive Definitions.
University of Edinburgh.
J. Brotherston, N. Gorogiannis & R. L. Petersen (2012):
A Generic Cyclic Theorem Prover.
In: APLAS-10 (10th Asian Symposium on Programming Languages and Systems),
LNCS 7705.
Springer,
pp. 350–367,
doi:10.1007/978-3-642-35182-2_25.
J. Brotherston & A. Simpson (2011):
Sequent calculi for induction and infinite descent.
Journal of Logic and Computation 21(6),
pp. 1177–1216,
doi:10.1093/logcom/exq052.
N. Dershowitz & G. Moser (2007):
The Hydra Battle Revisited.
Rewriting, Computation and Proof,
pp. 1–27,
doi:10.1007/978-3-540-73147-4_1.
G. Gentzen (1935):
Untersuchungen über das logische Schließen. I.
Mathematische Zeitschrift 39,
pp. 176–210,
doi:10.1007/BF01201353.
M. Michel (1988):
Complementation is more difficult with automata on infinite words.
Technical Report.
CNET.
S. Stratulat (2017):
Cyclic Proofs with Ordering Constraints.
In: R. A. Schmidt & C. Nalon: TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods),
LNAI 10501.
Springer,
pp. 311–327,
doi:10.1007/978-3-319-66902-1_19.
S. Stratulat (2018):
Validating Back-links of FOL_\voidb@x ID Cyclic Pre-proofs.
In: S. Berardi & S. van Bakel: CL&C'18 (Seventh International Workshop on Classical Logic and Computation),
EPTCS 281,
pp. 39–53,
doi:10.4204/EPTCS.281.4.
eptcs@eptcs.org