Revisión de Exercitium

Durante el curso 2013-14 inicié el blog Exercitium como complemento del curso de Informática de 1º del Grado de Matemáticas (I1M) de la Universidad de Sevilla.

El objetivo de Exercitium es plantear diariamente un problema para que los alumnos de I1M puedan practicar y escribir distintas soluciones en los comentarios.

Hasta el momento, en Exercitium se han publicado 514 ejercicios y 2.633 comentarios con soluciones. Además, según las estadísticas de WordPress, el blog ha tenido 118.249 visitas distribuidas como se muestra en la siguiente tabla

Revisión de Exercitium: Visitas mensualesVisitas mensuales

Como se observa, las visitas decrecen en verano (ya que no se proponen ejercicios desde julio hasta noviembre).

La distribución geográfica de las visitas se resume en el siguiente mapa de estadísticas de WordPress

Revisión de Exercitium: MapaMapa de visitas

Se observa que aunque en principio el blog era para las alumnos de I1M, las visitas no se han limitado a España sino que se ha extendido a otros países. Los países con mayor número de visitas son

País Visitas
España 94.730
México 4.754
Colombia 3.252
Estados Unidos 2.533
Perú 2.155
Argentina 1.923
Ecuador 1.666

Aprovechando el período de descanso estival he empezado una revisión de los problemas de Exercitium. La idea es escribir con Stack un proyecto por cada curso y publicarlo en GitHub. De momento, he publicado Exercitium1 con la revisión de los primeros ejercicios del curso 2013-14 y su correspondiente documentación en GitHUb.io.

En la revisión, estoy añadiéndole tests con DocTest, propiedades con QuickCheck y documentación con Haddock.

De esta forma, se facilita la descarga de los ejercicios y su uso. Para ello, basta

  • Instalar Stack (siguiendo sus instrucciones).
  • Descargar el proyecto usando una de las siguientes opciones
    • Descargar el fichero de Exercitium1, descomprimirlo y cambiar al directorio Exercitium1-master.
    • Clonar el repositorio de Exercitium1 con

      y cambiar al directorio Exercitium1.
  • Configurar el proyecto con
  • Construir el fichero con
  • Comprobar que todo está bien con

Durante este verano tengo previsto continuar las revisiones, publicarlas en GitHub y anunciarlas en Twitter con la etiqueta #RevExercitium.

I1M2015: El tipo abstracto de datos de grafos en Haskell

En la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de datos de los grafos y dos de sus implementaciones en Haskell: mediante vectores y matrices de adyacencia.

Además, hemos estudiado los algoritmos de recorrido de los grafos en profundidad y en anchura.

Las transparencias usadas en la clase son las páginas 1-39 del tema 22:

El código de la implementación de grafos mediante vectores de adyacencia es
Read More “I1M2015: El tipo abstracto de datos de grafos en Haskell”

LMF2016: Tableros semánticos

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se ha presentado un nuevo sistema deductivo: los tableros semánticos.

Hemos visto cómo los problemas de tautología y de consecuencia lógica se reducen a problemas de consistencia:

  1. F es una tautología syss {¬F} es inconsistente.
  2. F es consecuencia lógica de S syss S ∪ {¬F} es inconsistente.

Por tanto, para resolver ambos problemas basta con tener un procedimiento sistemático de búsqueda de modelos. Uno de dichos procedimientos es el de tableros semánticos.

Una ventaja de los tableros semánticos frente a la deducción natural es la reducción del número de reglas lo que facilita su automatización.

En la segunda parte de la clase se han estudiado los tableros semánticos de primer orden.

Las transparencias de esta clase son las de los temas 3 y 9.

Finalmente, se ha presentado el sistema Tree Proof Generator que busca automáticamente el tablero semántico correspondiente a la fórmula introducida.