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
styo16.pdf - Accepted Version
Restricted to registered users only until 16 June 2018.
Available under License BORIS Standard License.
Download (318kB) | Request a copy
1-s2.0-S0168007216300860-main.pdf - Published Version
Restricted to registered users only
Available under License Publisher holds Copyright.
Download (621kB) | Request a copy
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.
|Item Type:||Journal Article (Original Article)|
|Division/Institute:||08 Faculty of Science > Institute of Computer Science (INF)|
|UniBE Contributor:||Steila, Silvia|
|Subjects:||000 Computer science, knowledge & systems
500 Science > 510 Mathematics
|Date Deposited:||14 Feb 2017 11:33|
|Last Modified:||14 Feb 2017 11:36|