Abstract:
В статье освещены вопросы формализации итерационных вычислений. Составлена система первого
порядка, предназначенная для моделирования содержательных математических рассуждений. Описан
процесс построения логических выводов в этой системе, из которых затем извлекаются итерационные
программы для решения задач обработки массивов целых чисел. Приведены теоремы о конструктив-
ности выводов и правильности извлекаемых программ.
