LI2011: Estrategias y refinamiento de resolución proposicional
En la clase de hoy del curso Lógica Informática se hemos continuado la búsqueda de la automatización del razonamiento.
Después de haber visto en la clase anterior el algoritmo de resolución por saturación, hemos estudiado distintas estrategias cuyo objetivo es mejorar la búsqueda de la refutación por resilució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, como sistema de demostración por resolución se ha presentado el Prover9.
Como tarea se propone la resolución de los ejercicios del tema 5 del libro de ejercicios.
Las transparencias de esta clase son las páginas 25 a 37 del tema 5