Proof Pearl: Wellfounded Induction on the Ordinals up to Epsilon-0

This is the homepage of the paper Wellfounded Induction on the Ordinals up to Epsilon-0, authored by Matt Kaufmann, and Konrad Slind. The paper appeared at TPHOLs 2007.

Here is a PDF version of the paper. Here's the bibtex reference:

@InProceedings{e0:tphols07,
  author =       {M. Kaufmann and K. Slind},
  title =        {Proof Pearl: Wellfounded induction on the ordinals up to $\varepsilon_0$},
  booktitle =    {Theorem Proving in Higher Order Logics (TPHOLs 2007)},
  month =        {September},
  year =         2007,
  editor =       {K. Schneider},
  series =       {Lecture Notes in Computer Science},
  volume =       {???},
  publisher =    {Springer Verlag}
 }

The proof discussed in the paper is released with the HOL-4 implementation of higher order logic. The sources can be accessed in the (examples/acl2/ml) directory of the distribution.

Konrad Slind