El Método de Resolución [Robinson, 1965], es un intento de mecanizar el proceso de deducción natural de esa forma eficiente. Las demostraciones se consiguen utilizando el método refutativo (reducción al absurdo), es decir lo que intentamos es encontrar contradicciones.
Para probar una sentencia nos basta con demostrar que su negación nos lleva a una contradicción con las sentencias conocidas (es insatisfactible).
Si la negación de una sentencia entra en contradicción con los hechos de nuestra base de conocimiento es porque lo contrario, es decir, la sentencia original era verdadera y se puede deducir lógicamente de las sentencias que componen dicha base de conocimientos.
Búsqueda personalizada