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

Coinitial semantics for redecoration of triangular matrices

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Coinitial semantics for redecoration of triangular matrices.

Sus autores son Benedikt Ahrens y Régis Spadotti (del IRIT, Université Paul Sabatier).

Su resumen es

Infinite triangular matrices and, in particular, the redecoration operation on them, were studied by Matthes and Picard. In their work, redecoration is characterized as the cobind operation of what the authors call a “weak constructive comonad”.

In this work, we identify weak constructive comonads as an instance of the more general notion of relative comonad. Afterwards, building upon the work by Matthes and Picard, we give a category-theoretic characterisation of infinite triangular matrices—equiped with the canonical bisimulation relation and a compatible comonadic cobind operation—as the terminal object in some category.

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

Proof-by-instance for embedded network design

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Proof-by-instance for embedded network design.

Sus autores son

  • Marc Boyer (de ONERA – The French Aerospace Lab, Toulouse, France),
  • Loïc Fejoz (de RealTime-at-Work, Nancy, France) y
  • Stephan Merz (Inria & LORIA, Nancy, France).

Su resumen es

Proof-by-instance is a technique that ensures the correctness of the results of a computation rather than proving correct the tool carrying out the computation. We report here on the application of this idea to check the computations relevant for analyzing time bounds for AFDX networks. We have demonstrated the feasibility of the approach by applying a proof-of-concept implementation to an AFDX network of realistic size, and we outline the roadmap towards a mature industrial toolset. This approach should lead to a reduction of the time and cost of developing analysis tools used in the design of embedded networks where certification is mandatory.

El trabajo se presentó el 6 de febrero en el ERTS² 2014 Embedded Real Time Software And Systems.

A survey of axiom selection as a machine learning problem

PorJosé A. Alonso

Se ha publicado un artículo automatización del razonamiento en Isabelle/HOL titulado A survey of axiom selection as a machine learning problem.

Sus autores son

Su resumen es

Automatic theorem provers struggle to discharge proof obligations of interactive theorem provers. This is partly due to the large number of background facts that are passed to the automatic provers as axioms. Axiom selection algorithms predict the relevance of facts, thereby helping to reduce the search space of automatic provers. This paper presents an introduction to axiom selection as a machine learning problem and describes the challenges that distinguish it from other applications of machine learning.