¿Qué es?

es una manera de aplicar el Método de Resolución (Lógica) que pretende ahorrar tantas aplicaciones de la regla de resolución como sea posible.

¿Cómo es?