I1M2015: Definiciones de tipos en Haskell

En clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha visto

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos usando como ejemplo los naturales, las listas y los árboles

Se ha insistido en la metodología de definición de funciones recursivas sobre tipos de datos escribiendo una ecuación por cada uno de los constructores del tipo de dato.

Finalmente, se comentaron las distintas soluciones del problema Números muy divisibles por 3 y la comparación de la eficiencia.

Las transparencias usadas en la clase son las paginas 1 a 21 del tema 9:

LI2015: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)

En la primera parte de la clase de hoy del curso Lógica Informática hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland) para decidir la consistencia de conjuntos de cláusulas.

En la segunda parte, se ha explicado la solución del 3º ejercicio del primer examen del curso 2014-15:

Decidir, mediante tableros semánticos, si la fórmula

  • p → q ∨ s

es consecuencia lógica del conjunto de fórmulas

  • {q → s, ¬(¬p ∧ q)}.

En el caso de que no lo sea, dar un contramodelo.

Las transparencias utilizadas son las las página 1 a 12 del tema 6

LI2015: Estrategias de resolución proposicional

En la clase de hoy del curso Lógica Informática hemos continuado la búsqueda de la automatización del razonamiento.

Empezamos con un primer algoritmo de búsqueda de la cláusula vacía: el de saturación y dos mejoras: eliminación de tautologías y de subsumsución.

A continuación, hemos estudiado distintas estrategias cuyo objetivo es mejorar la búsqueda de la refutación por resolución.

Las estrategias estudiadas son la resolución positiva, la resolución negativa, la resolución unitaria, la resolución por entradas y la resolución lineal.

Además, se ha presentado la estrategia por pesos y propagación unitaria.

Finalmente, se ha mostrado el uso de Prover9 para decidir mediante resolución la validez de argumentos

En la segunda parte de la clase se han comentado las soluciones de los ejercicios 4.13 y 4.14 del libro de ejercicios

Las transparencias de esta clase son las páginas 18 a 37 del tema 5