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

PorJosé A. Alonso

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 los rectángulos.
  • El problema de las 4 reinas.
  • El problema de Ramsey.

Las transparencias utilizadas son las páginas 13 a 49 del tema 6
Read More “LI2013: Aplicaciones de la lógica proposicional con Prover9 y Mace4”

I1M2013: Tipos y clases en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado los tipos y las clases en Haskell. Los objetivos de tema son aprender

  • qué es un tipo,
  • cómo expresar que una expresión tiene un tipo determinado,
  • cómo preguntar a Haskell por el tipo de una expresión,
  • cómo determinar el tipo de una expresión,
  • cuáles son las ventajas de los tipos en programación,
  • cuáles son los tipos básicos (Bool, Char, String, Int, Integer, Float y Double),
  • cuáles son los tipos compuestos (listas, tuplas y funciones),
  • qué es el polimorfismo y la sobrecarga de funciones y
  • cuáles son las clases básicas (Eq, Ord, Show, Read, Num, Integral y Fractional), sus métodos e instancias.

Las transparencias usadas en la clase son las del tema 3:

LI2013: Estrategias de resolución proposicional

PorJosé A. Alonso

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. Las transparencias de esta clase son las páginas 18 a 37 del tema 5
Read More “LI2013: Estrategias de resolución proposicional”

I1M2013: Ejercicios de definiciones por comprensión (4)

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se han comentado las soluciones de los dos últimos ejercicios de la 4ª relación y de los 7 primeros de la 5ª relación. Ambas son sobre definiciones por comprensión.

Los ejercicios de la 4ª relación y sus soluciones se muestran a continuación
Read More “I1M2013: Ejercicios de definiciones por comprensión (4)”