Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Landau symbols en Isabelle/HOL.

Sus autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.

El trabajo se ha publicado en The Archive of Formal Proofs.

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

Este trabajo puede servir como lectura complementaria del curso de Razonamiento automático.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra titulado Representations of finite groups.

Su autor es Jeremy Sylvestre (de la Univ. de Alberta en Canadá).

Su resumen es

We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we develop the general theory of groups (relying on the group_add class for the basics), modules, and vector spaces, to the extent required for theory of group representations. We then provide formal proofs of several important introductory theorems in the subject, including Maschke’s theorem, Schur’s lemma, and Frobenius reciprocity. We also prove that every irreducible representation is isomorphic to a submodule of the group ring, leading to the fact that for a finite group there are only finitely many isomorphism classes of irreducible representations. In all of this, no restriction is made on the characteristic of the ring or field of scalars until the definition of a group representation, and then the only restriction made is that the characteristic must not divide the order of the group.

El trabajo se ha publicado el 12 de agosto en AFP (The Archive of Formal Proofs).

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 titulado Generalizing a mathematical analysis library in Isabelle/HOL.

Sus autores son Jesús Aransay y Jose Divasón de la Universidad de la Rioja.

Su resumen es

The HOL Multivariate Analysis Library (HMA) of Isabelle/HOL is focused on concrete types such as R, C and R n and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of HMA to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.

El trabajo se presentará en el NFM 2015 (The 7th NASA Formal Methods Symposium).