Implementación

• infiere con encadenamiento hacia atrás con búsqueda primero en profundidad (no completo)
• orden de busca en la conjunción de antecedentes: de izquierda a derecha
• orden de busca en las cláusulas de la KB: de primera a última
• no hace la parte occur-check de la rutina de unificación (unsound)
• punto de elección: en lugar de generar todas las respuestas para cada subobjetivo, el intérprete genera una respuesta y la promesa (punto de elección) de generar el resto cuando la respuesta actual sea explorada por completo (en busca primero en profundidad). Cuando esto ocurra se expandirá el punto de elección dando lugar a una nueva respuesta para el objetivo y un nuevo punto de elección
• en lugar de hacer sustituciones, implementa variables lógicas ligadas a un valor actual. Esas ligaduras definen la substitución válida en el camino actual. Cuando vuelve a un punto de elección puede necesitar desligar algunas variables (stack trail: push al ligar variables con unify-var, pop al desligarlas en los punto de elección)