1. 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.
  2. 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.
  3. J. Brotherston (2006): Sequent Calculus Proof Systems for Inductive Definitions. University of Edinburgh.
  4. 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.
  5. 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.
  6. 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.
  7. G. Gentzen (1935): Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift 39, pp. 176–210, doi:10.1007/BF01201353.
  8. M. Michel (1988): Complementation is more difficult with automata on infinite words. Technical Report. CNET.
  9. 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.
  10. 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.

Comments and questions to:
For website issues: