LI2015: Aplicaciones de la lógica proposicional con Prover9 y Mace4

En la clase de hoy del curso Lógica Informática hemos visto cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 para su solución.

Los problemas que se han visto son

  • El problema de los veraces y los mentirosos.
  • El problema de los animales.
  • El problema del coloreado del pentágono.
  • El problema del palomar.
  • El problema de las 4 reinas.

Las transparencias utilizadas son las del tema 6
Read More “LI2015: Aplicaciones de la lógica proposicional con Prover9 y Mace4”

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