I1M2013: El tipo abstracto de datos de grafos en Haskell

PorJosé A. Alonso

En la clase de hoy 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:
Read More “I1M2013: El tipo abstracto de datos de grafos en Haskell”

LMF2014: Ejercicios de deducción en lógica de primer orden con Isabelle/HOL (2)

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo demostrar mediante deducción natural teoremas de primer orden con Isabelle/HOL. En concreto, se han visto los ejercicios 13, 15, 16, 19, 21, 32 y 35 de la relación 6.

Los ejercicios y sus soluciones se muestran a continuación:
Read More “LMF2014: Ejercicios de deducción en lógica de primer orden con Isabelle/HOL (2)”

LMF2014: Tableros semánticos proposicionales

PorJosé A. Alonso

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

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

  • F es una tautología syss \{\neg F\} es inconsistente.
  • F es consecuencia lógica de S syss S \cup \{\neg 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 lo que facilita su automatización.

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

Las transparencias de esta clase son las del tema 3.
Read More “LMF2014: Tableros semánticos proposicionales”

LMF2014: Deducción natural en lógica de primer orden (2)

PorJosé A. Alonso

<

p>En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la segunda parte de la deducción natural en la lógica de primer orden. En concreto, la demostración de equivalencias lógicas y las reglas de la igualdad

<

p>Las transparencias de estas clases son las páginas 14 a 29 del tema 8.

<

p>A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es
Read More “LMF2014: Deducción natural en lógica de primer orden (2)”