En la sesión de hoy del Seminario de Lógica Computacional Alejandro Rodríguez Rodríguez ha explicado cómo demostrar en Coq propiedades de los números natuales por inducción.
La teoría, junto con los ejercicios, utilizados en la exposición son
Read More “SLC2018: Demostraciones por inducción en Coq”
En la sesión de hoy del Seminario de Lógica Computacional Ángel Ruiz Campos ha explicado la programación funcional en Coq.
La teoría, junto con los ejercicios, utilizados en la exposición son
Read More “SLC2018: Programación funcional en Coq”
En la sesión de hoy del Seminario de Lógica Computacional se ha presentado el seminario de este año comentando su objetivo, recursos y metodología.
El objetivo fundamental del seminario es el estudio de las relaciones entre lógica, demostración y programación. La explicación de los objetivos se ha basado en la presentación de Benjamin Pierce de su curso Software foundations.
Los recursos del seminario se encuentran en la página del Seminario entre los que se encuentran:
El principal texto del seminario es Software foundations (Volume 1: Logical foundations) y el sistema que se usará es Coq.
Respecto de metodología, las sesiones consistirán en exposiciones de los alumnos de la teoría, resolución colaborativa de los ejercicios y comentario de las soluciones publicadas.
En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con módulos en Haskell.
La explicación se ha basado en las tres primeras secciones del capítulo sobre módulos del libro ¡Aprende Haskell por el bien de todos!:
Las secciones son
+ Cargando módulos
+ El módulo Data.List
+ El módulo Data.Char
En la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la semántica de la lógica proposicional.
Se ha demostrado la equivalencia de los siguientes problemas
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabezas se ha explicado el uso del Gateway to Logic.
Las transparencias de esta clase son las páginas 30-34 del tema 1.