Автоматическое доказательство теорем — это краеугольный камень логического программирования, искусственного интеллекта и других современных направлений в программировании. Вообще говоря, может не существовать алгоритма, с помощью которого для произвольной формулы А через конечное число шагов можно определить, является ли A выводимой в исчислении ψ или нет. Однако, для некоторых простых формальных теорий (например исчисление высказываний) и некоторых простых классов формул (например прикладное исчисление предикатов с одним одноместным предикатом) алгоритмы автоматического доказательства теорем известны. Ниже, на примере исчисления высказываний, излагаются основы метода резолюций — классического и в то же время популярного метода автоматического доказательства теорем.