Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto (en inglés refutational complete and sound) para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacibles.
Puesto que toda proposición lógica se puede escribir en términos de disyunciones, conjunciones y negaciones lo anterior no supone una limitación del método más allá de transformar proposiciones lógicas.
La regla es bastante sencilla y un ejemplo muestra el razonamiento detrás de ella, de las siguientes dos oraciones: 'Juan va a al cine o Julia va a patinar' y 'Juan no va el cine o Jorge juega fútbol' podemos deducir la siguiente oración 'Julia va a patinar o Jorge juega fútbol' la razón es que puesto que Juan no puede al mismo tiempo ir y no ir al cine, para que las disyunciones anteriores sean ciertas se debe de cumplir alguna de las dos proposiciones: 'Julia va a patinar' o 'Jorge juega fútbol' o ambas.
Y una vez hallado susitituimos tal unificador en ambas cláusulas eliminando las literales correspondientes.
Hay dos asuntos a tomar en cuenta: los factores y renombrar variables.
Dos caminos surgieron, el primero tratar de entender qué proceso siguen las personas cuando crean demostraciones y hacer programas que emulen este comportamiento, el segundo usar de manera sistemática el trabajo ya desarrollado por los lógicos.