4.1. Постановка задачи

Алгоритм, который проверяет отношение для формулы S, множества формул Г и теории называется алгоритмом автоматического доказательства теорем (АТД).

В общем случае такой алгоритм невозможен, т. е. не существует алгоритма, который для любых S, Г и выдавал бы ответ «ДА», если Г |- S и «НЕТ» в противном случае. Но в некоторых случаях можно построить алгоритм, который применим не ко всем формулам теории (т. е. частичный алгоритм). Для некоторых простых формальных теорий (например, теории высказываний) алгоритмы АТД известны.

Пример. Для исчисления высказываний известно, что теоремами являются тавтологии, т. е. можно проверить является ли формула тавтологией с помощью таблиц истинности. Этот пример является примером доказательства теорем в теории £, но не является алгоритмом автоматического поиска вывода теорем из аксиоматической теории £.

Наиболее известный классический алгоритм АТД называется методом резолюций (МР). Для любого прикладного исчисления предикатов 1 порядка он дает ответ «ДА», если Г |- S и «НЕТ» или не выдает ответа в противном случае.