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:
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 ![]() | ![]() | C1: ¬p ![]() |
P2: | q ![]() ![]() | ![]() | C2: ¬q ![]() ![]() |
P3: | ¬s | ![]() | C3: ¬s |
¬C: | ¬(p ![]() | ![]() | C4: p |
![]() | C5: ¬r |
El proceso puede ser:
{C1, C4} | ![]() | C6: q |
{C2, C6} | ![]() | C7: s ![]() |
{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.