Последнее из трех рассматриваемых в данной главе семейств логических систем основано на резолюции. Как было показано в главе 7, пропозициональная резолюция — это полная процедура логического вывода для пропозициональной логики на основе опровержения. В этом разделе будет показано, как распространить резолюцию на логику первого порядка.

Проблема существования полных процедур доказательства всегда является предметом непосредственного внимания математиков. Если бы удалось найти полную процедуру доказательства для математических утверждений, это повлекло бы за собой два последствия: во-первых, вывод всех заключений мог бы осуществляться механически; во-вторых, всю математику можно было бы построить как логическое следствие некоторого множества фундаментальных аксиом. Поэтому вопрос о полноте доказательства стал в XX веке предметом наиболее важных математических работ. В 1930 году немецкий математик Курт Гёдель доказал первую теорему о полноте для логики первого порядка, согласно которой любое высказывание, являющееся следствием заданных аксиом, имеет конечное доказательство. (Но никакая действительно применимая на практике процедура доказательства не была найдена до тех пор, пока Дж.Э. Робинсон не опубликовал в 1965 году алгоритм резолюции.) В 1931 году Гёдель доказал еще более знаменитую теорему о неполноте. В этой теореме утверждается, что любая логическая система, которая включает принцип индукции (а без этого принципа удается построить лишь очень малую часть дискретной математики), обязательно является неполной. Поэтому существуют такие высказывания, которые следуют из заданных аксиом, но в рамках данной логической системы для них невозможно найти конечное доказательство. Иголка действительно может быть в метафорическом стоге сена, но ни одна процедура не позволяет гарантировать, что она будет найдена.

Несмотря на то, что теорема Гёделя о неполноте устанавливает определенные пределы, программы автоматического доказательства теорем на основе резолюции широко применялись и применяются для обоснования математических теорем, включая несколько таких теорем, для которых до сих пор не было известно доказательство. Кроме того, программы автоматического доказательства теорем успешно использовались для проверки проектов аппаратных средств, формирования логически правильных программ, а также во многих других приложениях.