En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la verificación de propiedades con QuickCheck y, como aplicación, se ha estudiado la verificación de la ordenación por mezcla siguiendo los ejercicios de la relación 9.
Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2013: Verificación de la ordenación por mezcla con QuickCheck”
Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A graph library for Isabelle.
Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).
Su resumen es
In contrast to other areas of such as analysis, number theory or probability theory, no standard library for graph theory has yet evolved for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs.
We use this library to formalize a characterization of Euler Digraphs and a to verify a method of checking Kuratowski subgraphs used in the LEDA library.
El código de la teoría en Isabelle se encuentra aquí.
En la clase de hoy del curso Lógica Informática se ha realizado el primer examen de la evaluación continua. Las soluciones se muestran a continuación
Read More “LI2013: 1º examen de la evaluación continua”
En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se han comentado las soluciones de los ejercicios de la 7ª relación y los 3 primeros de la 8ª sobre definiciones por recursión
Los ejercicios y sus soluciones se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por recursión”
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle/HOL.
Para ello, se visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 2a (que se corresponden con el capítulo 13 del libro de G. Hutton Programming in Haskell).
Las demostraciones estudiadas son las correspondientes a las 37 primeras páginas del tema 2a. Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL”