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]
Preview
Text
styo16.pdf - Accepted Version
Available under License Creative Commons: Attribution-Noncommercial-No Derivative Works (CC-BY-NC-ND).

Download (318kB) | Preview
[img] 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.

Item Type:

Journal Article (Original Article)

Division/Institute:

08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
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:

05 Dec 2022 14:57

Publisher DOI:

10.1016/j.apal.2016.06.001

ArXiv ID:

1512.08622v1

BORIS DOI:

10.7892/boris.85873

URI:

https://boris.unibe.ch/id/eprint/85873

Actions (login required)

Edit item Edit item
Provide Feedback