Validating Back-links of FOLID Cyclic Pre-proofs

[1] P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739-782. North Holland, 1977. https://doi.org/10.1016/S0049-237X(08)71120-0 [OpenAIRE]

[2] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[3] S. Berardi and M. Tatsuta. Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. In CMCS'18, LNCS, 2018. to appear. [OpenAIRE]

[4] J. Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Proceedings of TABLEAUX14, volume 3702 of LNAI, pages 78-92. Springer-Verlag, 2005. https://doi.org/10.1007/11554554_8 [OpenAIRE]

[5] J. Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. [OpenAIRE]

[6] J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS-10 (10th Asian Symposium on Programming Languages and Systems), volume 7705 of LNCS, pages 350-367. Springer, 2012. https://doi.org/10.1007/978-3-642-35182-2_25 [OpenAIRE]

[7] J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. https://doi.org/10.1093/logcom/exq052

[8] G. Gentzen. Untersuchungen u¨ber das logische Schließen. I. Mathematische Zeitschrift, 39:176-210, 1935.

[9] O. Kupferman and M. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic (TOCL), 2(3):408-429, 2001. https://doi.org/10.1145/377978.377993

[10] S. Stratulat. A unified view of induction reasoning for first-order logic. In A. Voronkov, editor, Turing100 (The Alan Turing Centenary Conference), volume 10 of EPiC Series, pages 326-352. EasyChair, 2012. https://doi.org/10.29007/nsx4 [OpenAIRE]

[11] S. Stratulat. Cyclic proofs with ordering constraints. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017, volume 10501 of LNAI, pages 311-327. Springer, 2017. https://doi.org/10.1007/ 978-3-319-66902-1_19 [OpenAIRE]

[12] S. Stratulat. Mechanically certifying formula-based Noetherian induction reasoning. Journal of Symbolic Computation, 80, Part 1:209-249, 2017. https://doi.org/10.1016/j.jsc.2016.07.014 [OpenAIRE]