Skip to Main content Skip to Navigation
Conference papers

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-02044649
Contributor : Hal Ifip <>
Submitted on : Thursday, February 21, 2019 - 3:41:24 PM
Last modification on : Thursday, February 21, 2019 - 3:48:39 PM
Long-term archiving on: : Wednesday, May 22, 2019 - 9:13:09 PM

File

473364_1_En_3_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Stefano Berardi, Makoto Tatsuta. Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.13-33, ⟨10.1007/978-3-030-00389-0_3⟩. ⟨hal-02044649⟩

Share

Metrics

Record views

87

Files downloads

22