0 = {{P},¬C}, es decir, el conjunto formado por las premisas
(en forma clausulada) y la negación de la conclusión (de esta negación resultará, en
general, un conjunto de cláusulas). El proceso seguirá su curso, de acuerdo con la
estrategia de control adoptada, aplicando siempre la única regla: la de resolución. Si C
es una conclusión correcta y el sistema deductivo es completo el proceso terminará
encontrando la cláusula vacía, 
. Tal cosa ocurrirá cuando como resolvente
aparezca un literal L y se observe que ¬L ya estaba incluido en : la resolución
de los dos produce como resolvente la cláusula vacía, que corresponde a la
contradicción.
Como decíamos en el Apartado 3.7.1, la estrategia más sencilla es la de la búsqueda en extensión. Se demuestra que con esta estrategia un sistema deductivo para la lógica de proposiciones con resolución y refutación:
0 
SI se
cumple que 0
(es decir, si el sistema refuta C, 0 es inconsistente,
lo que significa que las premisas {P} implican C), y siempre que 0
resulta que 0 SI (es decir, si las premisas implican la conclusión el
sistema encuentra la cláusula vacía).
0 /
el proceso termina sin generar la cláusula vacía
Pero tanto la complejidad espacial como la temporal de una búsqueda en extensión
son del orden de O(bd), donde b es el factor de ramificación y d la profundidad de la
solución (número de resoluciones necesario para llegar a ella). En este caso, además, b
crece proporcionalmente con la profundidad de la búsqueda. En efecto, si el estado
inicial, 0, contiene N = n + m cláusulas (n procedentes de las n premisas y m de la
conclusión negada), puede haber hasta N × (N - 1)/2 resolventes, cada una de
ellas susceptible de, a su vez, resolverse con otra o con alguna cláusula de 0,
etc.
De entre las muchas estrategias propuestas para reducir la complejidad de la
búsqueda comentaremos solamente la más utilizada, que se llama resolución lineal con
la entrada: siempre se toma una generatriz perteneciente a la primera parte de 0
({P}) y otra de la segunda (¬C) o descendiente de ella. Es decir, una generatriz
procedente de las premisas iniciales (que forma el llamado conjunto de entrada) y otra
que procede directa o indirectamente de la conclusión negada.
Tomando como ejemplo el del Apartado 3.8.3:
| P1: | p  q |  | C1: ¬p  q |
| P2: | q (¬s r) | | C2: ¬q s r |
| P3: | ¬s | | C3: ¬s |
| ¬C: | ¬(p r) | | C4: p |
| C5: ¬r |
El proceso puede ser:
| {C1, C4} | | C6: q |
| {C2, C6} | | C7: s r |
| {C3, C7} | | C8: r |
| {C4, C8} | | |
El problema con esta estrategia es que no es completa. Consideremos esta inferencia deductiva:
P1: p q
P2: ¬p q
P3: q p
C: p 
q
Pasando las premisas y la conclusión negada a forma clausulada resultan la cláusulas:
C1: ¬p q
C2: p q
C3: p ¬q
C4: ¬p ¬q
La estrategia obliga a que una de las cláusulas generatrices sea C1, C2 o C3, y la otra C4 o descendiente de ella.
{C1,C4} C5: ¬p
{C2,C4} p ¬p, q ¬q (tautologías)
{C3,C4} C6: ¬q
{C1,C6} C5
{C2,C5} C7: q
Aunque está claro que hay una refutación entre C6 y C7, las condiciones de la estrategia impiden aplicarla.
Sin embargo, esta estrategia es completa cuando se impone una cierta restricción sobre la forma de las cláusulas: que sean cláusulas de Horn.
DIT-ETSIT-UPM