A cyclic proof system gives us another way of representing inductive and coinductive definitions and efficient proof search. Podelski-Rybalchenko termination theorem is important for program termination analysis. This paper first shows that Heyting arithmetic HA proves Kleene-Brouwer theorem for induction and Podelski-Rybalchenko theorem for induction. Then by using this theorem this paper proves the equivalence between the provability of the intuitionistic cyclic proof system and that of the intuitionistic system of Martin-Lof’s inductive definitions when both systems contain HA.
CITATION STYLE
Berardi, S., & Tatsuta, M. (2018). Intuitionistic podelski-rybalchenko theorem and equivalence between inductive definitions and cyclic proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11202 LNCS, pp. 13–33). Springer Verlag. https://doi.org/10.1007/978-3-030-00389-0_3
Mendeley helps you to discover research relevant for your work.