Стаття присвячена опису дедуктивного принципу синтезу програм з використанням методу резолюції на прикладі отримання алгоритму сортування. У статті показано принцип, що дає можливість отримувати твердження-відповіді на основі використання методу побудови дерев спростування та доведення.
Статья посвящена описанию дедуктивного принципа синтеза программ с использованием метода резолюции на примере получения алгоритма сортировки. В статье показан принцип, что дает возможность получать утверждение-ответы на основе использования метода построения деревьев опровержения идоказательства.
This article is dedicated to the deductive program synthesis with using of resolution method on an example of sorting algorithm creation. In the article there is a shown principle that allows getting assertions-answers on the basis of method refutation and leading trees construction using.
