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.

Properties of random graphs – subgraph containment

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre grafos titulado Properties of random graphs – subgraph containment.

Sus autor es Lars Hupel (de la Univ. Politécnica de Munich).

Su resumen es

Random graphs have been introduced by Erdös and Rényi in [1]. They describe a probability space where, for a fixed number of vertices, each possible edge is present with a certain probability independent from other edges, but with the same probability for each edge. They study what properties emerge when increasing the number of vertices, or as they call it, “the evolution of such a random graph”. The theorem which we will prove here is a slightly different version from that in the first section of that paper.

Here, we are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges, which is usually undesired since it degrades the performance of many algorithms, whereas a low edge probability might result in a disconnected graph. The central theorem determines a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.

The proof is outlined in [2, §11.4] and [3, §3]. The work is based on the comprehensive formalization of probability theory in Isabelle/HOL and on a previous definition of graphs in a work by Noschinski [4]. There, Noschinski formalized the proof that graphs with arbitrarily large girth and chromatic number exist. While the proof in this paper uses a different approach, the definition of a probability space on edges turned out to be quite useful.

El trabajo se ha publicado en Archive of Formal Proofs

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