Синтез программ дедуктивный — автоматический синтез программ в котором используется формальный метод построения программ; вывод программы из заданной спецификации рассматривается как задача конструктивного доказательства существования нужного решения. В ходе реализации С.П.Д. часто используются методы автоматического доказательства теорем в исчислении предикатов первого порядка.
[Толковый словарь по искусственному интеллекту / Авторы-составители А.Н. Аверкин, М.Г. Гаазе-Рапопорт, Д.А. Поспелов. М.: Радио и связь, 1992. — 256 с.]