Resolución (lógica)

Resolución solamente funciona cuando se escriben las proposiciones en términos de premisas que constan solamente de disyunciones de literales. Puesto que toda proposición lógica se puede escribir en términos de disyunciones, conjunciones y negaciones lo anterior no supone una limitación del método más allá de transformar proposiciones lógicas. Las proposiciones escritas en esta forma se les denomina cláusulas.

La regla es bastante sencilla y un ejemplo muestra el razonamiento detrás de ella, de las siguientes dos oraciones: 'Juan va a al cine o Julia va a patinar' y 'Juan no va el cine o Jorge juega fútbol' podemos deducir la siguiente oración 'Julia va a patinar o Jorge juega fútbol' la razón es que puesto que Juan no puede al mismo tiempo ir y no ir al cine, para que las disyunciones anteriores sean ciertas se debe de cumplir alguna de las dos proposiciones: 'Julia va a patinar' o 'Jorge juega fútbol' o ambas.

En general esta regla se escribe de la siguiente forma:

${\displaystyle {\frac {p_{1}\lor \ldots \vee p_{i}\vee \ldots \lor p_{n},\quad q_{1}\lor \ldots \vee q_{j}\vee \ldots \lor q_{m}}{p_{1}\lor \ldots \lor p_{i-1}\lor p_{i+1}\lor \ldots \lor p_{n}\lor q_{1}\lor \ldots \lor q_{j-1}\lor q_{j+1}\lor \ldots \lor q_{m}}}}$

donde:

${\displaystyle \forall i\in \left\lbrace 1,2,\ldots ,n\right\rbrace p_{i}}$ es un literal

${\displaystyle \forall j\in \left\lbrace 1,2,\ldots ,m\right\rbrace q_{j}}$ es un literal

y ${\displaystyle p_{i}}$ es la negación (complementario) de ${\displaystyle q_{j}}$

Para poder emplear esta regla tenemos que pasar todas nuestra proposiciones a la forma normal de cláusulas o forma estándar de cláusulas. Una fórmula de lógica de primer orden se puede transformar a la forma normal de cláusulas mediante los siguientes pasos: 1. Pasar la fórmula a la forma prenexa. 2. Pasar la matriz (es decir, la parte de la fórmula que no incluye a los cuantificadores) a la forma conjuntiva normal. 3. Skolemizar.

Una vez escrita en esta forma los cuantificadores universales no se escriben.

Para usar resolución primero procedemos a hallar el unificador más general de dos cláusulas. Y una vez hallado susitituimos tal unificador en ambas cláusulas eliminando las literales correspondientes. Hay dos asuntos a tomar en cuenta: los factores y renombrar variables.

El poder de cómputo ha propiciado que ciertas áreas nuevas se desarrollaran en el siglo XX, la demostración automatizada de teoremas surgió de la motivación por crear programas de computadora que emularan las habilidades humanas de razonamiento. Dos caminos surgieron, el primero tratar de entender qué proceso siguen las personas cuando crean demostraciones y hacer programas que emulen este comportamiento, el segundo usar de manera sistemática el trabajo ya desarrollado por los lógicos.

De este segundo camino se crearon los demostradores automatizados de teoremas, se hicieron y se siguen haciendo varios intentos, uno de los que han tenido más influencia es el método de resolución introducido por Robinson en 1965. Robinson encontró una sola regla de inferencia, fácil de implementar por una computadora, que era completa para la lógica de primer orden.

• Chang, Chin-Liang (1973). Symbolic Logic and Mechanical Theorem Proving (1 edición). Academic Press.
• Robinson,A. y Voronkov,A. (editores.), ed. (2001). Handbook of Automated Reasoning Volume I. Elsevier y MIT Press.
• Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.
• Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.
• Fitting, Melvin (1996). First-Order Logic and Automated Theorem Proving (2 edición). Springer. Archivado desde el original el 21 de mayo de 2010. Consultado el 29 de abril de 2012.