En la clase de hoy del curso Lógica matemática y fundamentos hemos continuado la búsqueda de métodos automáticos para el problema TAUT (i.e. decidir si una fórmula dada es una tautología) y el problema SAT (i.e decidir si una fórmula dada es satisfacible).
Comenzamos observando que:
Por tanto,
- para la solución del problema TAUT sólo nos falta un procedimiento mecánico que dada una fórmula calcule otra que sea equivalente a la dada y que esté en FNC y
- para la solución del problema SAT sólo nos falta un procedimiento mecánico que dada una fórmula calcule otra que sea equivalente a la dada y que esté en FND.
Mostramos las reglas equivalencia para el cálculo de los formas normales y los procedimientos de decisión para los porblemas TAUT y SAT.
Por último, vemos cómo el método de los tableros semánticos proporciona otro procedimiento de cálculo de las formas normales.
Las transparencias de esta clase son las del tema 4
Read More “LMF2014: Formales normales conjuntivas y disyuntivas”