Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre automatización del razonamiento titulado Truly modular (co)datatypes for Isabelle/HOL.

Sus autores son

• Jasmin Christian Blanchette (de la Technische Universität München, Alemania),
• Johannes Hölzl (de la Technische Universität München, Alemania),
• Andreas Lochbihler (del ETH Zurich, Suiza),
• Lorenz Panny (de la Technische Universität München, Alemania),
• Andrei Popescu (de la Technische Universität München, Alemania) y
• Dmitriy Traytel (de la Technische Universität München, Alemania).

Su resumen es

“We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion–corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle’s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.”

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

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

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).