¿Qué es?
Es un procedimiento de demostración sistemático que permite ser mecanizado con relativa simplicidad. método de resolución utiliza una única regla (Regla de Resolución):
Si se tiene una disyunción que contiene un enunciado A, y también se tiene otra disyunción que contiene la negación de este enunciado A, entonces es lícito obtener una disyunción que contiene todos los disyuntandos de las dos anteriores, excepto la pareja A y ﹁A porque se aniquilan mutuamente.
A v B
﹁A v C
-------
B v C
No obstante, es conveniente atender a los siguientes casos:
- Disjunciones de un único disjuntando. Los dos disjuntandos se aniquilan mútuamente y el resultado es una contradicción.
A
﹁A
-------
CONTRADICCION!
- Si hay más de una pareja de disjuntandos que pueden aniquilarse mútumente, sólo uno de ellos desaparece y los demás permanecen en la disjunción resultante.
A v B A v B
﹁A v﹁B ﹁A v﹁B
------- == -------
A v﹁A B v﹁B
TEOREMA! Y dado que siempre se puede obtener un teorema (principio de libre inclusión), aplicaciones de una regla como ésta no sirven de nada y hay que evitarlas.
¿Cómo lo aplicamos?
El método de resolución utiliza una única estrategia: la reducción al absurdo.
Para demostrar que de unas premisas se desprende una conclusión, la reducción al absurdo prueba que de las mismas premisas y de la negación de la conclusión se desprende una contradicción. Si la contradicción se encuentra, el razonamiento es correcto; si la contradicción no se encuentra, entonces no es correcto.
A1,..., An ⊢ B si y sólo si, A1,... An, ﹁B ⊢ Contradicción
Pero previamente, dado que la regla de resolución sólo se aplica a disyunciones, debemos construir la FNC de todas las premisas y de la negación de la conclusión. Una vez hecho esto, las conjunciones se deben eliminar.
Con todo lo anterior, ya podemos aplicar validar o refutar un razonamiento : A1,..., An ∴ B aplicando los siguientes pasos:
-
Considerar A1,…, An, ﹁B (las premisas y la negación de la conclusión).
-
Construir la FNC de cada una de las Ai y de ﹁B y eliminar todas las conjunciones. El resultado será un conjunto de cláusulas.
-
Aplicar la regla de resolución a las cláusulas encontradas en el punto anterior y a todas las que resulten, hasta que o bien se encuentre una contradicción, o bien ya no se pueda continuar aplicando la regla. Las cláusulas repetidas y los teoremas, si aparecen, no se tienen en consideración.
-
Si se ha encontrado una contradicción, entonces el razonamiento es correcto (A1,…, An ⊢ B); en caso contrario, el razonamiento no es correcto.
Los pasos que hay que hacer hasta llegar a la contradicción se representan en forma de árbol binario invertido
Leti. logica de enunciados (p. 67). Kindle Edition.