TEMA 7: INFERENCIA EN LÓGICA DE PRIMER ORDEN

Alvaro Barreiro. Dept. Computación. Universidade da Coruña

• Reglas de inferencia con cuantificadores
• Modus Ponens generalizado
• Encadenamiento hacia delante y encadenamiento hacia atrás
• Completitud y decidibilidad
• Resolución: un procedimiento de inferencia completo
  • 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
• About this document ...