Cálculo de Predicados de Primer Orden

El Cálculo de Predicados de Primer Orden es útil para IA como medio de representación e inferencia.

La IA no garantiza siempre una respuesta (no es determinista, no representa procedimiento efectivo)

• Ejemplo
• Marco era un hombre
• Marco era pompeyano
• Todos los pompeyanos eran romanos
• César fue un gobernante
• Todos los romanos o eran leales a César o lo odiaban
• Todo el mundo es leal a alguien
• La gente sólo intenta a asesinar los gobernantes a los que no es leal
• Marco intentó asesinar a César

Resolución                                    

   

Es una regla de inferencia usada en la deducción computacional, debido a que es eficiente ya que trabaja sobre sentencias que han sido transformadas a una forma canónica llamadas cláusulas disyuntivas.
Este proceso de resolución obtiene demostraciones por refutación. Es decir, para probar una proposición (su validez) se intenta demostrar que su negación lleva a una contradicción con las proposiciones conocidas (es decir es insatisfactible).