SLC2018: Presentación del “Seminario de Lógica Computacional” (2018)

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:

  • Temas: Donde se irán publicando las teorías de los temas conforme se vayan exponiendo.
  • Ejercicios: Donde se publicarán las relaciones de ejercicios para resolverlos de manera colaborativa.
  • Documentación: Donde se publicarán enlaces a lecturas recomendadas.
  • Sistemas: Donde se publicarán enlaces a los sistemas utilizados.

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.

LMF2017: Sintaxis y semántica de la lógica proposicional (2)

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

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

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.

LMF2017: Sintaxis y semántica de la lógica proposicional

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

Finalmente, se ha iniciado el estudio de la semántica de la lógica proposicional definiendo los booleanos, las interpretaciones, las funciones de verdad de las conectivas y mostrando cómo a partir de dichos conceptos se puede calcular el valor de verdad de una fórmula respecto de una interpretación.

A partir de lo anterior se han estudiado los modelos de fórmulas, la clasificación semántica de fórmulas (satisfacibles, insatisfacibles, tautologías, contradictorias y contingentes), los problemas SAT y TAUT. Finalmente, se han visto dos algoritmos para la solución de los problemas SAT y TAUT: tablas de verdad y método de Quine.

Otros conceptos definidos son equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y consecuencia lógica.

Finalmente, se ha hecho un ejemplo de formalización usando APLI2

Las transparencias de esta clase son las páginas 1-30 del tema 1.

I1M2017: Programación con Haskell en la Red usando Repl.it

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha explicado cómo programar con Haskell sólo de una conexión a la Red (ya sea en un ordenador que no tiene instalado Haskell, una tableta o un teléfono).

Para ello basta usar el sistema Repl.it que proporciona una sesión en la Red con Haskell (en concreto, la versión 8.0.1 de GHCi).

Como ejemplo se realizó la sesión grabada en el vídeo Haskell con Repl.it.