3.7.1. Procesos deductivos

• El estado del proceso en cada momento es un conjunto de sentencias que denotaremos con el símbolo «» .
• El estado inicial es el conjunto de premisas: ₀ = {P₁,P₂...}.
• Los operadores que aplicados a un estado generan el estado siguiente son las reglas de inferencia.
• Una transición es un paso de un estado al estado siguiente mediante la aplicación de una regla de inferencia: _{i R.I.i+1}.
• El proceso termina cuando la conclusión buscada, C, está incluida en el estado: C _final.

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:

• ¿qué regla de inferencia aplicar?
• ¿a qué sentencias de ?

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.

 DIT-ETSIT-UPM