LMF2013: Estrategias de resolución proposicional
En la clase de hoy del curso Lógica matemática y fundamentos 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 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, como sistema de demostración por resolución se ha presentado el Prover9.
Las transparencias de esta clase son las páginas 25 a 37 del tema 5