کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6861248 | 675268 | 2015 | 30 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Beyond polynomials and Peano arithmetic-automation of elementary and ordinal interpretations
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Beyond polynomials and Peano arithmetic-automation of elementary and ordinal interpretations Beyond polynomials and Peano arithmetic-automation of elementary and ordinal interpretations](/preview/png/6861248.png)
چکیده انگلیسی
Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel implementation of algebras based on ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by Touzet (1998) of the battle of Hercules and Hydra as well as a (corrected) encoding by Beklemishev (2006) of the Worm battle, two further systems which have been out of reach for automatic tools, until now. Based on our ideas of implementing ordinal algebras we also present a new approach for the automation of elementary interpretations for termination analysis.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 69, JulyâAugust 2015, Pages 129-158
Journal: Journal of Symbolic Computation - Volume 69, JulyâAugust 2015, Pages 129-158
نویسندگان
Harald Zankl, Sarah Winkler, Aart Middeldorp,