RESOLUCION

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.