Reverse mathematical bounds for the Termination Theorem

Steila, Silvia; Yokoyama, Keita (2016). Reverse mathematical bounds for the Termination Theorem. Annals of pure and applied logic, 167(12), pp. 1213-1241. Elsevier 10.1016/j.apal.2016.06.001

Preview	Text styo16.pdf - Accepted Version Available under License Creative Commons: Attribution-Noncommercial-No Derivative Works (CC-BY-NC-ND). Download (318kB) | Preview
	Text 1-s2.0-S0168007216300860-main.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (621kB)

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.

Interest & Impact

Downloads

199 since deposited on 14 Feb 2017
33 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item