Reverse mathematical bounds for the termination theorem

DOI10.1016/J.APAL.2016.06.001zbMATH Open1402.03023arXiv1512.08622OpenAlexW2963942212MaRDI QIDQ324248FDOQ324248

Authors: Silvia Steila, Keita Yokoyama 

Publication date: 10 October 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1512.08622

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

zbMATH Keywords

reverse mathematicsRamsey's theoremParis Harrington's theoremtermination theorem

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Foundations of classical theories (including reverse mathematics) (03B30) Logic in computer science (03B70) Ramsey theory (05D10) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Rapidly growing Ramsey functions
• Hierarchies of number-theoretic functions. I
• The proof-theoretic strength of Ramsey's theorem for pairs and two colors
• Proof-theoretic analysis of termination proofs
• Reverse mathematics and Peano categoricity
• Parameter free induction and provably total computable functions
• The strength of infinitary Ramseyan principles can be accessed by their densities
• The theory of well-quasi-ordering: a frequently discovered concept
• Measure theory and weak König's lemma
• On the strength of Ramsey's theorem for pairs
• Decidability of termination of grid string rewriting rules
• \(\mathsf{RT}_{2}^{2}\) does not imply \(\mathsf{WKL}_{0}\)
• Stop when you are almost-full. Adventures in constructive termination
• Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic
• Transition invariants and transition predicate abstraction for program termination
• Slicing the truth. On the computable and reverse mathematics of combinatorial principles
• Combinatorial principles weaker than Ramsey's Theorem for pairs
• Title not available (Why is that?)
• Some independence results for Peano arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\varPi^1_1\)-conservation of combinatorial principles weaker than Ramsey's theorem for pairs
• Title not available (Why is that?)
• An intuitionistic version of Ramsey's theorem and its use in program termination
• On the Ramseyan factorization theorem
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• Separating principles below Ramsey's theorem for pairs
• Ramsey's theorem and recursion theory

Cited In (7)

• Dickson's lemma and weak Ramsey theory
• Partial orders and immunity in reverse mathematics
• The strength of the SCT criterion
• Program termination and well partial orderings
• The proof-theoretic strength of Ramsey's theorem for pairs and two colors
• An analysis of the Podelski-Rybalchenko termination theorem via bar recursion
• A combinatorial bound for a restricted form of the termination theorem

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)