PTTP

PTTP (Prolog Technology Theorem Prover ), cambios sobre Prolog

• meter de nuevo la parte occurr-check en la rutina de unificación
• cambiar búsqueda primero en profundidad por profundización iterativa (completa)
• permite literales negados; se implementa una rutina para probar P y otra para probar notP
• una cláusula con n átomos se almacena como n reglas distintas
• la inferencia es completa por la regla de resolución de entrada lineal: si el objetivo actual unifica con la negación de uno de los objetivos de la pila, entonces puede considerarse probado