LMF2016: Tableros semánticos

PorJosé A. Alonso

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.

I1M2015: El tipo abstracto de datos de los montículos en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado el tipo abstracto de los montículos, su implementación en Haskell mediante tipo de datos algebraicos y su aplicación para las colas de prioridad.

Las transparencias usadas en la clase son las del tema 20.

El código correspondiente es
Read More “I1M2015: El tipo abstracto de datos de los montículos en Haskell”

I1M2015: Resolución de una ecuación con factoriales en Haskell

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 28, cuyo objetivo es resolver la ecuación a! * b! = a! + b! + c!, donde a, b y c son números naturales.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2015: Resolución de una ecuación con factoriales en Haskell”