Хотя Маккарти [1009] предложил использовать логику первого порядка для представления знаний и формирования рассуждений в искусственном интеллекте, первые подобные системы были разработаны логиками, заинтересованными в получении средств автоматического доказательства математических теорем. Впервые применение метода пропозиционализации и теоремы Эрбрана предложено Абрахамом Робинсоном, а Гилмор [556] написал первую программу, основанную на этом подходе. Дэвис и Патнем [336] применили форму представления в виде импликационных выражений и разработали программу, в которой предпринимались попытки поиска противоречий путем подстановки элементов универсума Эрбрана вместо переменных для получения базовых выражений, а затем поиска пропозициональных противоречивостей среди этих базовых выражений. Правиц [1234] разработал ключевую идею, позволяющую использовать для управления процессом поиска тенденцию к обнаружению пропозициональных противоречивостей и вырабатывать термы из универсума Эрбрана, только если это необходимо для определения пропозициональной противоречивости. После дальнейшей разработки этой идеи другими исследователями Дж.Э. Робинсон (который не связан родством с Абрахамом Робинсоном) пришел к созданию метода резолюции [1298]. Примерно в то же время советским исследователем С. Масловым [994], [995] на основе немного иных принципов был разработан так называемый инверсный метод, который характеризуется некоторыми вычислительными преимуществами над пропозиционализацией. Метод соединения Вольфганга Бибеля [123] может рассматриваться как расширение этого подхода.

После разработки метода резолюции исследования в области логического вывода первого порядка стали развиваться в нескольких разных направлениях. В искусственном интеллекте метод резолюции применялся для создания систем поиска ответов на вопросы Корделлом Грином и Бертрамом Рафаэлем [593]. Несколько менее формальный подход был принят Карлом Хьюиттом [651]. Разработанный им язык Planner, хотя и не был полностью реализован, явился предшественником логического программирования и включал директивы для прямого и обратного логического вывода и для отрицания как недостижения цели. А подмножество этого языка, известное как Micro-Planner [1475], было реализовано и использовалось в системе понимания естественного языка Shrdlu [1601]. В ранних реализациях систем искусственного интеллекта большие усилия направлялись на разработку структур данных, которые должны были обеспечить эффективную выборку фактов; эти работы описаны в книгах по программированию для искусственного интеллекта [240], [479], [1148].