Reseña: “Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de conjuntos titulado Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁.

Sus autores son Michael Norrish (del (Canberra Research Lab., NICTA) y Brian Huffman (de Galois, Inc.).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀ , the existence of normalforms, and the validation of algorithms used in the ACL2 theorem-proving system.

El código de las correspondientes teorías en HOL se encuentra aquí.