A pesar de su indudable interés matemático, el teorema de Gödel, por sí solo, nos
sirve de poco en la práctica: existe una demostración de C (siempre que C sea una
conclusión válida), pero ¿cómo se construye?, ¿cuál es el conjunto de reglas de
inferencia a aplicar? En 1965 ([84]) Robinson propuso la regla de resolución y
demostró que sólo con ella y con un algoritmo de refutación y búsqueda en extensión
resulta un sistema deductivo consistente y completo para la lógica de predicados
(aplicando también la regla de particularización de un universal). Obsérvese que si la
sentencia C a demostrar (la «consulta»
) contiene variables, el algoritmo nos dará todos los valores de esas variables para los
cuales 
0
C. No importa que, por ser semidecidible, no pueda encontrar aquellos
valores para los cuales no es el caso que 0
C (aunque en la práctica nunca
podremos estar seguros de sí es que no hay más valores o que aún no los ha
encontrado).
En las páginas siguientes extenderemos a la lógica de predicados lo explicado para la de proposiciones en los Apartados 3.8.1 a 3.8.6
DIT-ETSIT-UPM