Las bases de la resolución

El procedimiento de resolución es un proceso iterativo en el cual, en cada paso se comparan dos cláusulas llamadas cláusulas padres produciendo una nueva cláusula que se ha inferido de ellas llamada resolvente.

Las cláusulas padres deberán ser tales que tengan ambas un mismo literal, una afirmada y la otra negado.

   Ejemplo

• Es invierno o es verano
• No es invierno o hace frío

Resolución en Lógica Proposicional

    Sea ф la conclusión,  Σ el conjunto de los argumentos:

1. Convertir todas las proposiciones en Σ a su forma de cláusulas
2. Negar ф y convertir el resultado en cláusula. Agregar la o las cláusulas resultantes al conjunto de cláusulas obtenidas en 1
3. Hasta encontrar una contradicción o no se pueda seguir avanzando:

• Seleccionar dos cláusulas que tienen como literales una L y la otra ¬L
• Resolverlas juntas. El resolvente será la disyunción de todos los literales que contienen los padres excepto L y ¬L
• Si el resolvente es la cláusula vacía, es que se ha encontrado una contradicción. Si no lo es agregarla al conjunto de cláusulas disponibles.

Resolución en Lógica de Predicados

1. Convertir todas las expresiones de Σ a Cláusulas
2. Negar ф y convertir el resultado en cláusula  y agregarlo al conjunto obtenido en 1
3. Repetir hasta encontrar una contradicción o no se pueda seguir:

a) Seleccionar cláusulas padres
b) Si existe un par de literales L1 y L2, uno en cada cláusula padre, tal que L1 y ¬L2 sean unificables, entonces obtener el resolvente mediante:

• La disyunción de los literales de ambas cláusulas padres excepto L1 y L2
• Usar la sustitución que unifica L1 y ¬L2 para crear el resolvente
• Si existe más de un par de literales complementarios, sólo se elimina uno

c) Si el resolvente es la cláusula vacía, se ha encontrado contradicción, sino agregarla al conjunto de cláusulas.