Resolución guiada por metas
Compara una refutación general con la reducción lineal que usa Prolog sobre cláusulas de Horn.
Resolución general
Prolog / SLD
Paso de resolución
⊕
↓
Anterior
Siguiente