Reseña: Cardinals in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado Cardinals in Isabelle/HOL.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Univ. Técnica de Munich).

Su resumen es

We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced is the inability of higher-order logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation that identifies ordinals with wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss two applications of this general theory in formal developments.

El trabajo se presentará el martes 15 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).

Towards abstract and executable multivariate polynomials in Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra computacional titulado Towards abstract and executable multivariate polynomials in Isabelle.

Sus autores son

Su resumen es

This work in progress report envisions a library for multivariate polynomials developed jointly by experts from computer theorem proving (CTP) and computer algebra (CA). The urgency of verified algorithms has been recognised in the field of CA, but the cultural gap to CTP is considerable; CA users expect high usability and efficiency. This work collects the needs of CA experts and reports on the design of a proof-of-concept prototype in Isabelle/HOL. The CA requirements have not yet been fully settled, and its development is still at an early stage. The authors hope for lively discussions at the Isabelle Workshop.

El trabajo se presentará el próximo domingo en el Isabelle Workshop del Vienna Summer of Logic (VSL2014).

Lecturas del Grupo de Lógica Computacional (del 15 al 29 de junio)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas las dos últimas semanas (del 15 al 19 de junio) en la lista de correo del grupo de lógica computacional

La recopilación está ordenada por la fecha de su publicación en Twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.