LMF2017: Lógica y programación

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se han comentado algunas relaciones entre la lógica y la programación.

En primer lugar, a partir del artículo The Curry-Howard correspondence between programs and proofs se han comentado cómo los tipos se corresponden con las fórmulas y la existencia de funciones de un tipo dado se corresponde con la veracidad de su fórmula.

Como lectura complementario se ha recomendado el artículo El isomorfismo de Curry-Howard y una introducción a Coq.

Para analizar la distancia del lenguaje matemático a los de programación, se ha comentado el artículo From math to machine: translating a function to machine code que partiendo de la definición matemática del factorial expica su representación en un lenguaje funcional (Haskell), en uno imperativo (C), en ensamblador y en código máquina.

LMF2017: Sintaxis de la lógica proposicional y representación del conocimiento

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se han comentados las soluciones propuestas de la 1ª relación de ejercicios sobre sintaxis de la lógica proposicional y representación del conocimiento.

En la segunda parte, se ha explicado cómo hacer demostraciones por deducción natural usando Pandora. Su uso se muestra en este vídeo.

Finalmente, se ha propuesto la 2ª relación de ejercicios.

LMF2017: Deducción natural proposicional (1)

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica proposicional.

Se ha comenzado repasando las cuestiones fundamentales estudiadas en el tema 1:

  • ¿Qué es una fórmula?
  • ¿Qué significa que una fórmula sea verdadera?

y planteando una nueva cuestión

  • ¿Qué es un teorema?

para responderla, de forma análoga al uso de modelos para responder a la 2ª cuestión, se comenta el uso de las demostraciones.

El primer método de demostración que se presenta es el de deducción natural. Se han estudiado las siguientes reglas:

  • Reglas de la conjunción
  • Reglas de la doble negación
  • Regla de eliminación del condicional
  • Regla derivada de modus tollens (MT)
  • Regla de introducción del condicional
  • Reglas de la disyunción

Las transparencias de esta clase son las 1-12 del tema 2.

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

En la primera parte de 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

La clase de hoy del curso Lógica matemática y fundamentos ha tenido dos partes.

En la primera parte se ha presentado un panorama de la lógica y sus aplicaciones. También se ha explicado cómo formalizar en lógica proposicional argumentos expresados en lenguaje natural. Para practicar con las formalizaciones se ha presentado APLI2.

En la segunda parte 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.

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