En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios sobre la numeración de los números racionales en Haskell de la relación 25.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2014: Ejercicios sobre la numeración de los racionales en Haskell”
En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha comentado las soluciones de los ejercicios de la relación 24 que consiste en la implementación del TAD de los grafos mediante lista.
Las soluciones de los ejercicios de la relación es el siguiente
Read More “I1M2014: Ejercicios sobre la implementación del TAD de grafos mediante listas”
En la clase de hoy del curso Lógica matemática y fundamentos se han comentado soluciones de los ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL.
Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la automática.
La teoría con la relación de ejercicios y sus soluciones es la siguiente
Read More “LMF2015: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL”
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica de primer orden.
Las transparencias de estas clases son las del tema 8.
A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es
Read More “LMF2015: Deducción natural en lógica de primer orden”
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).