Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

A Mechanizable First-Order Theory of Ordinals

Reviewed Paper In Proceedings

Author(s):Peter H. Schmitt
In:26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017)
Publisher:Springer
Series:LNCS
Volume:10501
Year:2017
Pages: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)},
  place     = {Bras{\'{\i}}lia, Brazil},
  date      = {September 25-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.}
}