Reverse mathematical bounds for the termination theorem
From MaRDI portal
(Redirected from Publication:324248)
Abstract: In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey's Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko's Termination Theorem we can extract some information about termination bounds.
Recommendations
- Reverse mathematics and order theoretic fixed point theorems
- A combinatorial bound for a restricted form of the termination theorem
- The reverse mathematics of the Tietze extension theorem
- Lebesgue Convergence Theorems and Reverse Mathematics
- Degrees bounding principles and universal instances in reverse mathematics
- Pincherle's theorem in reverse mathematics and computability theory
- Reverse mathematics of separably closed sets
- Computer Science Logic
- Rudin's Lemma and Reverse Mathematics
- The Brouwer invariance theorems in reverse mathematics
Cites work
- scientific article; zbMATH DE number 3914378 (Why is no real title available?)
- scientific article; zbMATH DE number 3689386 (Why is no real title available?)
- scientific article; zbMATH DE number 1215495 (Why is no real title available?)
- scientific article; zbMATH DE number 1226875 (Why is no real title available?)
- scientific article; zbMATH DE number 512769 (Why is no real title available?)
- scientific article; zbMATH DE number 1144041 (Why is no real title available?)
- scientific article; zbMATH DE number 3446873 (Why is no real title available?)
- An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
- An intuitionistic version of Ramsey's theorem and its use in program termination
- Combinatorial principles weaker than Ramsey's Theorem for pairs
- Decidability of termination of grid string rewriting rules
- Hierarchies of number-theoretic functions. I
- Measure theory and weak König's lemma
- On the Ramseyan factorization theorem
- On the strength of Ramsey's theorem for pairs
- Parameter free induction and provably total computable functions
- Proof-theoretic analysis of termination proofs
- Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic
- Ramsey's theorem and recursion theory
- Rapidly growing Ramsey functions
- Reverse mathematics and Peano categoricity
- Separating principles below Ramsey's theorem for pairs
- Slicing the truth. On the computable and reverse mathematics of combinatorial principles
- Some independence results for Peano arithmetic
- Stop when you are almost-full. Adventures in constructive termination
- The proof-theoretic strength of Ramsey's theorem for pairs and two colors
- The strength of infinitary Ramseyan principles can be accessed by their densities
- The theory of well-quasi-ordering: a frequently discovered concept
- Transition invariants and transition predicate abstraction for program termination
- \(\mathsf{RT}_{2}^{2}\) does not imply \(\mathsf{WKL}_{0}\)
- \(\varPi^1_1\)-conservation of combinatorial principles weaker than Ramsey's theorem for pairs
Cited in
(7)- Dickson's lemma and weak Ramsey theory
- The proof-theoretic strength of Ramsey's theorem for pairs and two colors
- An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
- Partial orders and immunity in reverse mathematics
- A combinatorial bound for a restricted form of the termination theorem
- The strength of the SCT criterion
- Program termination and well partial orderings
This page was built for publication: Reverse mathematical bounds for the termination theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q324248)
