4.8.5. Sistemas deductivos con resolución y refutación
Es aplicable aquí todo lo dicho en el Apartado 3.8.5, salvo una consecuencia de que
la lógica de predicados es, en general, indecidible: si 0/ (donde 0 incluye las
premisas y la conclusión negada) el proceso puede no terminar.
La estrategia de resolución lineal con la entrada es también incompleta en general,
pero completa para cláusulas de Horn.
0 /
(donde 
DIT-ETSIT-UPM