JAIST Repository >
b. 情報科学研究科・情報科学系 >
b10. 学術雑誌論文等 >
b10-1. 雑誌掲載論文 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/15307
|
タイトル: | Reverse mathematical bounds for the Termination Theorem |
著者: | Steila, Silvia Yokoyama, Keita |
キーワード: | Reverse Mathematics Ramsey's Theorem Termination Theorem Paris Harrington's Theorem |
発行日: | 2016-06-15 |
出版者: | Elsevier |
誌名: | Annals of Pure and Applied Logic |
巻: | 167 |
号: | 12 |
開始ページ: | 1213 |
終了ページ: | 1241 |
DOI: | 10.1016/j.apal.2016.06.001 |
抄録: | 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. |
Rights: | Copyright (C)2016, Elsevier. Licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International license (CC BY-NC-ND 4.0). [http://creativecommons.org/licenses/by-nc-nd/4.0/] NOTICE: This is the author's version of a work accepted for publication by Elsevier. Silvia Steila and Keita Yokoyama, Annals of Pure and Applied Logic, 167(12), 2016, 1213-1241, http://dx.doi.org/10.1016/j.apal.2016.06.001 |
URI: | http://hdl.handle.net/10119/15307 |
資料タイプ: | author |
出現コレクション: | b10-1. 雑誌掲載論文 (Journal Articles)
|
このアイテムのファイル:
ファイル |
記述 |
サイズ | 形式 |
22910.pdf | | 479Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|