Формальный синтез алгоритмов был одним из первых направлений использования средств автоматического доказательства теорем, как и было намечено Кордел-лом Грином [591], который опирался на идеи, высказанные ранее Саймоном [1416]. Общий замысел состоит в том, что должна быть доказана теорема с утверждением, что "существует программа р, удовлетворяющая некоторой спецификации". Если удается ограничить это доказательство конструктивной формой, то появляется возможность извлечь из результатов доказательства требуемую программу. Хотя полностью автоматизированный дедуктивный синтез, как стало называться это направление, еще не осуществим применительно к программированию задач общего назначения, дедуктивный синтез, управляемый вручную, оказался успешным при проектировании нескольких новейших и сложнейших алгоритмов. Кроме того, активной областью исследования является синтез программ специального назначения. В области синтеза аппаратных средств программа автоматического доказательства теорем Aura применялась для проектирования схем, оказавшихся более компактными по сравнению с разработанными во всех предыдущих проектах [1609]. Для многих проектов логических схем достаточно применить пропозициональную логику, поскольку множество интересующих высказываний является фиксированным благодаря конечным размерам множества схемных элементов. В наши дни применение пропозиционального логического вывода в аппаратном синтезе является стандартным методом, имеющим много крупномасштабных областей использования (см., например, работу Новика и др. [1149]).

Те же методы теперь начинают также применяться для проверки программного обеспечения с помощью таких систем, как программа проверки моделей Spin [672]. Например, с ее помощью была проверена до и после полета программа управления космическим аппаратом Remote Agent [633].