ПОДСИСТЕМА ОБУЧЕНИЯ И КОНТРОЛЯ ПРЕОБРАЗОВАНИЙ УТВЕРЖДЕНИЙ В ЯЗЫКЕ ЛОГИКИ ПРЕДИКАТОВ

Abstract

Рассматривается задача создания обучающей подсистемы в рамках методологии ОККАМ [1] для обучения алгоритму сокращенного переборного поиска опровергающего набора, используемому для доказательства утверждений в языке логики предикатов. Описывается подход к анализу ошибок обучаемого, возникающих в процессе решения данной задачи. Особое внимание обращается на обеспечение полноты контроля и адекватности комментариев в случае обнаружения ошибки.