A Mechanizable First-Order Theory of Ordinals

@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.}
}