resolución es completa por refutación: si un conjunto de sentencias es no verificable, entonces la resolución probará una contradicción. La resolución no puede generar todas las consecuencias lógicas de un conjunto de sentencias, pero puede establecer si una determinada sentencia es una consecuencia lógica del conjunto