A Mechanizable First-Order Theory of Ordinals. In: Schmidt, Renate A.; Nalon, Claudia (Ed.): Automated Reasoning with Analytic Tableaux and Related Methods - 26th
International Conference, {TABLEAUX} 2017, Brasilia, Brazil,
September 25-28, 2017, Proceedings, pp. 331–346, Springer, 2017, ISBN: 978-3-319-66901-4.
Abstract
We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the
KeY program verification system which is in turn used to prove termination of a Java program computing
the Goodstein sequences.
Links
BibTeX (Download)
@inproceedings{Schmitt2017,
title = {A Mechanizable First-Order Theory of Ordinals},
author = {Peter H. Schmitt},
editor = {Renate A. Schmidt and Claudia Nalon},
url = {https://www.key-project.org/papers/ordinal-numbers},
doi = {10.1007/978-3-319-66902-1_20},
isbn = {978-3-319-66901-4},
year = {2017},
date = {2017-09-06},
urldate = {2017-09-06},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 26th
International Conference, {TABLEAUX} 2017, Brasilia, Brazil,
September 25-28, 2017, Proceedings},
volume = {10501},
pages = {331--346},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the
KeY program verification system which is in turn used to prove termination of a Java program computing
the Goodstein sequences.},
keywords = {theorem proving},
pubstate = {published},
tppubtype = {inproceedings}
}