Resolución (lógica) es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. 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. Por otro lado si el conjunto de proposiciones de hecho es satisfacible, puede o no terminar en una cantidad finita de pasos una demostración por resolución, generalmente lo que sucede es que se asigna un tiempo límite para hallar si un conjunto es insatisfacible o no.
