Одни из первых работ в области автоматизированного синтеза программ были выполнены Саймоном [1416], Грином [591], а также Манна и Ваддингером [976]. В трансформационной системе Бурстолла и Дарлингтона [211] используется формирование рассуждений с учетом отношения равенства для синтеза рекурсивных программ. Одной из самых сильных современных систем является Kids [1435], [1436]; она действует в качестве помощника эксперта. В [979] приведено учебное введение с описанием современного состояния дел в этой области, в котором основное внимание уделено описанию собственного дедуктивного подхода этих авторов. В книге Automating Software Design [954] собрано множество статей из этой области. Обзор примеров использования логики в проектировании аппаратных средств приведен в [791]; в [267] рассматривается применение метода проверки по модели для диагностирования аппаратных средств.

Хорошим справочником по темам полноты и неразрешимости является книга Computability and Logic [ 150]. Многие ранние статьи в области математической логики можно найти в книге From Frege to Godel: A Source Book in Mathematical Logic [1532]. Официальным журналом для публикаций в области чистой математической логики (в отличие от автоматизированного дедуктивного логического вывода) является The Journal of Symbolic Logic. К числу учебников, посвященных автоматизированному дедуктивному логическому выводу, относятся классическая книга Symbolic Logic and Mechanical Theorem Proving [233], а также более новые работы [124], [776] и [1618]. Антология Automation of Reasoning [1408] включает много важных ранних статей по автоматизированному дедуктивному логическому выводу. Другие исторические обзоры приведены в [206] и [949]. Основным журналом для публикаций в области автоматического доказательства теорем является Journal of Automated Reasoning, а главной конференцией — ежегодно проводимая конференция Conference on Automated Deduction (CADE). Кроме того, исследования в области автоматического доказательства теорем тесно связаны с работами по использованию логики при анализе программ и языков программирования, которым посвящена основная конференция Logic in Computer Science.