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

[img] Text
styo16.pdf - Accepted Version
Restricted to registered users only until 16 June 2018.
Available under License BORIS Standard License.

Download (318kB) | Request a copy
[img] Text
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
ISSN: 0168-0072
Publisher: Elsevier
Language: English
Submitter: Lukas Jaun
Date Deposited: 14 Feb 2017 11:33
Last Modified: 14 Feb 2017 11:36
Publisher DOI: 10.1016/j.apal.2016.06.001
ArXiv ID: 1512.08622v1
BORIS DOI: 10.7892/boris.85873

Actions (login required)

Edit item Edit item
Provide Feedback