A Mechanizable First-Order Theory of Ordinals

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Peter H. Schmitt
In:26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017)
Verleger:Springer
Reihe:LNCS
Band:10501
Jahr:2017
Seiten:331-346
DOI:10.1007/978-3-319-66902-1_20

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.

BibTeX

@InProceedings{schmitt2017,
  author    = {Peter H. Schmitt},
  editor    = {Renate A. Schmidt and Cl{\'a}udia Nalon},
  title     = {A Mechanizable First-Order Theory of Ordinals},
  booktitle = {26th International Conference on Automated
               Reasoning with Analytic Tableaux and Related
               Methods ({TABLEAUX} 2017)},
  venue     = {Bras{\'{\i}}lia, Brazil},
  eventdate = {2017-09-25/2017-09-28},
  year      = {2017},
  month     = aug,
  series    = {LNCS},
  volume    = {10501},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-66902-1_20},
  pages     = {331--346},
  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.}
}