Rosapolis

pero tenía que escribirlo en un lugar público ahora mismo o explotaba (y era muy largo para el Buzz).

Instrucciones para alcanzar un estado de euforia absoluta programando un automatic theorem prover

Empezar a depurar un predicado en Prolog a las 8 de la mañana usando trace/0 porque tus inconscientes inclinaciones al sadomasoquismo camufladas en forma de pereza te impiden intentar hacer funcionar el graphic debugger en Mac OS X.

Sentir como el cerebro se te va calentando de retener en la cabeza sustituciones, ramas del árbol de backtracking y cláusulas con 6 variables amablemente renombradas por el intérprete como _G393, _G394, _G395...

Reprimir los tremendos impulsos animales de estrellar el portátil contra la pared cuando Prolog no explora las 3 alternativas que llevan a completar el tablero a profundidad 5, volviendo arriba del todo en el árbol e incrementando la profundidad a 6 para no acabar nunca.

Probar 80 soluciones a cuál más absurda y seguir observando el maldito fail en las trazas durante 2 horas más, mientras imaginas tu futuro en una cámara de aislamiento con una camisa de fuerza gritando creep en medio de convulsiones.

Darte cuenta de que lo que tú creías que era un complejo error introducido por un corte en una rama debido a la implementación de SWI-Prolog de la estructura if-then-else es en realidad tu brillante implementación, producto de un momento de aguda estupidez de esos que ocurren contadas veces en la vida de una persona, del predicado assert_clauses/1 en el que compruebas si una cláusula C=[H|B] existe previamente usando cla(H,B,_) en vez de subsumed(C), dando carta blanca a Prolog para que instancie tus variables en medio de una orgía unificadora que finaliza con tu conjunto inicial de cláusulas reducido a la mitad y convertido naturalmente en satisfactible.

Arreglarlo y comprobar que ahora sí funciona y que encuentra un tablero cerrado para el conjunto de más abajo muchísimo más rápido que leanCoP.


p( a, b, c ).
p( X, e, X ).
p( e, X, X ).
p( X, X, e ).
- p( b, a, c ).
- p( U, V, Y ) | - p( X, U, Z ) | - p( Z, V, W ) | p( X, Y, W ).
- p( U, V, Y ) | - p( X, U, Z ) | - p( X, Y, W ) | p( Z, V, W ).