Resolución: un procedimiento de inferencia completo

• procedimiento de inferencia completo y sano (sound) para FOL
• mas potente que Modus Ponens, permite derivar implicaciones

• La regla de inferencia
• Formas canónicas
• Prueba
• Conversión a forma normal
• Ejemplo del procedimiento de conversión y de la prueba por refutación
• Tratamiento de la igualdad: demodulación
• Estrategias de resolución
• Completitud de la resolución
• Teorema de la incompletitud de Gödel