LI2011-12: 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 los rectángulos.
- El problema de las 4 reinas.
- El problema de Ramsey.
Como tarea pendiente se propone la solución de problemas análogos siguiendo la misma estructura que los anteriores:
- Enunciado.
- Simbolización.
- Representación.
- Búsqueda de la prueba (con Prover9) o de modelos (con Mace4).
- Conclusión.
Las transparencias utilizadas son las del tema 5b
Los códigos de los ejemplos se encuentran aquí.