В продолжение обсуждения архитектуры интеллектуальных обучающих систем (ИОС), рассмотрим их методическое обеспечение и некоторые аспекты реализации. Интересной и недавно разработанной ИОС, основанной на автоматическом доказательстве теорем (АДТ), является «Why2-Atlas». Эта система содержит 7 вычислительных задач по вводному курсу механики. Дидактический цикл выглядит так: система выдает ученику одну из задач и просит его ввести ответ с объяснением. Затем она обсуждает с ним этот ответ и, после обсуждения, как правило, просит уточнить объяснение. Последний шаг повторяется, пока не будут устранены все недочеты в ответе обучаемого.