На первых порах основные усилия ученых были сосредоточены на проблемах полноты. Вслед за появлением оригинальной статьи Робинсона в работах [1619] и [1620] были предложены правила демодуляции и парамодуляции для формирования рассуждений с учетом отношения равенства. Эти правила были также разработаны независимо в контексте систем перезаписи термов [811]. Внедрение средств формирования рассуждений с учетом отношения равенства в алгоритм унификации было осуществлено Гордоном Плоткиным [1217]; применение таких средств было также предусмотрено в языке Qlisp [1339]. В [752] приведен обзор средств унификации с учетом отношения равенства на основе процедур перезаписи термов. Эффективные алгоритмы для стандартной унификации были разработаны Мартелли и Монтанари [989], а также Патерсоном и Вегманом [1181].

Кроме средств формирования рассуждений с учетом отношения равенства, в программы автоматического доказательства теорем были включены всевозможные процедуры принятия решений специального назначения. В [1120] предложена получившая широкое распространение схема интеграции подобных процедур в общую схему формирования рассуждений; к другим методам относятся "резолюция теории" Стикеля [1462] и "специальные отношения" Манна и Валдингера [978].

Для метода резолюции был предложен целый ряд стратегий управления, начиная со стратегии предпочтения единичного выражения [1616]. В [1617] была предложена стратегия с использованием множества поддержки, которая позволяет обеспечить определенную целенаправленность резолюции. Линейная резолюция впервые была предложена в [948]. В [537, глава 5] приведен краткий, но исчерпывающий анализ всего разнообразия стратегий управления.

В [602] описана одна из первых программ автоматического доказательства теорем, Sam, которая позволила решить одну из открытых проблем в теории решеток. В [1621] приведен краткий обзор того, какой вклад был внесен с помощью программы автоматического доказательства теорем Aura в решение открытых проблем в различных областях математики и логики. Это описание продолжено в [1018], где перечислены достижения программы Otter, преемника программы Aura, в решении открытых проблем. В [1563] описана программа Spass— одна из сильнейших современных программ автоматического доказательства теорем. Основным справочником по программе автоматического доказательства теорем Бойера—Мура является книга A Computational Logic [165]. В [1463] рассматривается система РТТР (Prolog Technology Theorem Prover), в которой сочетаются преимущества компиляции Prolog с полнотой устранения моделей [947]. Еще одной широко применяемой программой автоматического доказательства теорем, основанной на этом подходе, является SETHEO [915]; она способна выполнять несколько миллионов логических выводов в секунду на рабочих станциях модели 2000. Эффективной программой автоматического доказательства теорем, реализованной всего лишь в 25 строках на языке Prolog, является LeanTaP [91].