RA2014: Razonamiento estructurado sobre programas con Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.

Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.

Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2014: Razonamiento estructurado sobre programas con Isabelle/HOL”

LI2014: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland) y aplicaciones proposicionales

PorJosé A. Alonso

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, 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 del tema 6
Read More “LI2014: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland) y aplicaciones proposicionales”

LI2014: 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.

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

Las transparencias de esta clase son las páginas 18 a 37 del tema 5
Read More “LI2014: Estrategias de resolución proposicional”