Рассмотрена задача компьютерной поддержки решения математических задач в математических учебных системах. Ход решения задачи определяется как последовательность преобразований формулы логики предикатов, построенной по условию задачи, т.е. логический вывод. Поддержка хода решения осуществляется в двух режимах: режиме проверки правильности шага решения и режиме автоматического его выполнения.
