En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar la corrección del algoritmo de ordenación por mezcla.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2016: Verificación de la ordenación por mezcla con Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar la corrección del algoritmo de inserción.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2016: Verificación de la ordenación por inserción con Isabelle/HOL”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos el problema de las reinas (consistente en colocar N reinas en un tablero de dimensiones N por N de forma que no se encuentren más de una en la misma línea: horizontal, vertical o diagonal).
Los apuntes correspondientes a la clase son
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos desarrollado un programa en Haskell para resolver los problemas aritméticos del concurso Cifras y letras que consisten en dada una sucesión de números naturales y un número objetivo, intentar construir una expresión cuyo valor es el objetivo combinando los números de la sucesión usando suma, resta, multiplicación, división y paréntesis. Además, cada número de la sucesión puede usarse como máximo una vez y todos los números, incluyendo los resultados intermedios tienen que ser enteros positivos (1,2,3,…).
Por ejemplo, dada la sucesión 1, 3, 7, 10, 25, 50 y el objetivo 765, una solución es (1+50)x(25−10). Para el problema anterior existen 780 soluciones. En cambio, con la sucesión anterior y el objetivo 831, no hay solución.
Se empieza formalizando el problema y definiendo una función para reconcer las soluciones. A continuación, se presentan tres soluciones: la primera por fuerza bruta, la segunda mediante generación y evaluación y la tercera con simplificaciones algebraicas. Se termina con una comparación de las tres soluciones.
Los apuntes correspondientes a la clase son
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalized linear algebra over elementary divisor rings in Coq.
Sus autores son
Su resumen es
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bézout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension ≤1 and well-founded strict divisibility.
El trabajo se ha publicado en Logical Methods in Computer Science (Volume 12, Issue 2).
El código de las correspondientes teorías en Coq se encuentra aquí.