¿Qué es?
Es una técnica que garantiza la sistematicidad de la resolución lineal.
Es una técnica algorítmica bastante conocida. En el contexto de la programación es habitual designarla con el término inglés backtracking que, a menudo, se traduce por ‘vuelta atrás’ o ‘prueba y error’.
¿Cómo es?
Esta técnica consiste en anotar todas las decisiones que se toman y, para cada decisión, las posibles alternativas. Cuando se llega a un punto en el que no se puede continuar, se revoca la última de las decisiones tomadas que todavía tenga una alternativa no considerada y se continúa a partir de aquel punto.
Cuando se han considerado todas las alternativas y no se ha llegado a encontrar una contracción, entonces se puede afirmar que el razonamiento no es correcto.
Además de la imposibilidad de encontrar una cláusula que elimine el literal de más a la derecha de la última cláusula troncal, hay dos situaciones más que obligan a replantear la última decisión:
-
La aparición de un teorema como cláusula troncal
-
La repetición de una cláusula aparecida previamente en el mismo árbol, como vemos a continuación:
