![atras](izda.png)
![adelante (solo si previamente se ha ido
atras)](dcha.png)
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 /![|=](rcsi112x.png)
(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.
![atras](izda.png)
DIT-ETSIT-UPM