En las clase hoy Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 11 a 24 sobre vectores y matrices en Haskell de la relación 24.
Los ejercicios y su solución se muestran a continuación de los 24 primeros ejercicios de la relación es
Read More “I1M2013: Ejercicios sobre vectores y matrices en Haskell (2)”
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:
es una tautología syss 
es inconsistente.
es consecuencia lógica de 
syss 
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”
<
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)”
En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.
Una tabla (array en inglés y tableau en francés) es una colección de elementos (valores) a los que se accede mediante sus índices.
El contenido de la clase ha sido el siguiente:
Read More “I1M2013: El TAD (tipo abstracto de datos) de las tablas en Haskell”
Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional o en mi página de twitter desde la anterior recopilación.
La recopilación está ordenada por la fecha de su publicación en la lista o en twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
Read More “Lecturas del Grupo de Lógica Computacional (de julio de 2013 a marzo de 2014)”