В подходе на основе натуральной дедукции (natural deduction), который был введен Герхардом Генценом [541] и Станиславом Яськовским [725], основное внимание было сосредоточено не на аксиоматических системах, а на правилах логического вывода. Натуральная дедукция получила название "натуральной", поскольку в ней не требуется преобразование в нормальную форму (неудобную для восприятия человеком), а также в связи с тем, что в ней применяются такие правила логического вывода, которые кажутся естественными для людей. Правитц [1235] посвятил описанию натуральной дедукции целую книгу. Галье [515] применил подход Гентцена для разъяснения теоретических основ автоматизированной дедукции.

Крайне важным этапом в разработке глубокого математического анализа логики первого порядка явилось изобретение формы представления в виде импликационных выражений (clausal form). Уайтхед и Рассел [1584] описали так называемые правила прохождения (rules of passage) (фактически этот термин принадлежит Эрбрану [650]), которые используются для перемещения кванторов в переднюю часть формул. Торальфом Сколемом [1424] были достаточно своевременно предложены ско-лемовские константы и сколемовские функции. Общая процедура сколемизации, наряду с важным понятием универсума Эрбрана, описана в [1425].

Крайне важную роль в разработке автоматизированных методов формирования рассуждений, как до, так и после введения Робинсоном правила резолюции, играет теорема Эрбрана, названная в честь французского логика Жака Эрбрана [650]. Это отражается в применяемом нами термине "универсум Эрбрана", а не "универсум Сколема", даже несмотря на то, что это понятие в действительности было открыто Сколемом. Кроме того, Эрбран может считаться изобретателем операции унификации. Гёдель [565], опираясь на идеи Сколема и Эрбрана, сумел показать, что для логики первого порядка имеется полная процедура доказательства. Алан Тьюринг [1518] и Алонсо Черч [255] практически одновременно продемонстрировали, используя очень разные доказательства, что задача определения общезначимости в логике первого порядка не имеет решения. В превосходной книге Эндертона [438] все эти результаты описаны в строгой, но труднодоступной для понимания манере.