Sólo consideraremos aquí procesos monótonos (Apartado 2.4.1), en los que
i
i+1
Así planteado, el problema de la demostración es un problema de búsqueda, en el
que hay que decidir una estrategia de control que en cada estado permita responder
a estas dos cuestiones:
La más ingenua de las estrategias de control es la que corresponde a una búsqueda
en extensión: aplicar, una a una, cada regla a cada sentencia o parejas de sentencias,
para obtener todos los estados siguiente posibles de «profundidad 1»
, repetirlo sobre estos estados, y así sucesivamente, comprobando en cada paso la
condición de terminación (C
final). La complejidad tanto temporal como espacial
(recursos de tiempo de ejecución y memoria) de esta estrategia la hace inaplicable
incluso en lógica de proposiciones (excepto para problemas con un número muy
reducido de variables proposicionales). En el Apartado 3.8.5 volveremos sobre este
asunto.