Программа ТеорМат

Программа ТеорМат является средством для активного и глубокого изучения теоретических основ математического анализа. В отличие от любого традиционного учебника, который предполагает чтение (пассивное изучение), программа ТеорМат предполагает самостоятельное доказательство теорем и самостоятельное решение теоретических задач (активное изучение). Для этого программа ТеорМат создает среду, удобную для доказательства теорем и следит за корректностью доказательства. Среда для доказательства теорем состоит из следующих элементов

• язык ТеорМат;
• поле доказательства;
• действия пользователя;
• действия компьютера.

Язык ТеорМат близок к общепринятой форме записи математических выражений. В частности, элементами языка являются кванторы, символы математических операций, математические понятия "сходимость", "ограниченность" и т.п. Например, теорема о пределе суммы двух последовательностей на языке ТеорМат записывается в следующем виде:

Все математические утверждения (определения, аксиомы, теоремы и т.д.), записанные на языке ТеорМат, составляют книгу математических утверждений.

Поле доказательства - это визуальное представление текущего состояния доказательства в терминах "дано" и "требуется доказать". Поле доказательства состоит из четырех разделов: "Данные объекты", "Данные условия", "Искомые объекты", "Доказываемые условия". Поле доказательства служит не только для визуализации состояния доказательства, оно также является рабочим столом для действий пользователя.

Действие пользователя может быть связано или не связано с условием, содержащимся в поле доказательства. Выполнение действия, не связанного с условием поля доказательства, осуществляется с помощью меню стандартных действий и методов, состоящем из следующих пунктов

• определить объект;
• применить утверждение;
• рассмотреть случаи;
• доказать вспомогательное условие;
• метод доказательства от противного;
• метод математической индукции.

Для выполнения действия, связанного с некоторым условием поля доказательства, пользователь нажимает на кнопку, находящуюся слева от этого условия. В ответ компьютер предлагает список преобразований, которые могут быть выполнены с этим условием. Далее пользователь выбирает преобразование из предложенного списка, а компьютер выполняет выбранное преобразование.

Действие компьютера - это автоматические преобразования поля доказательства и преобразования, выполняемые по требованию пользователя.

Перед началом доказательства компьютер, исходя из формулировки доказываемого утверждения, выполняя автоматические преобразования, формирует поле доказательства. Например, в начале доказательства теоремы (1) поле доказательства будет иметь вид

В ходе доказательства компьютер следит за корректностью и выполняет тривиальные автоматические преобразования, облегчающие процесс доказательства. Пользователь может посмотреть, какие автоматические преобразования выполнил компьютер на данном шаге.

Если доказаны все условия раздела "Доказываемые условия" или получено противоречие, доказательство считается успешно завершенным. Протокол доказательства можно сохранить в файл, по которому компьютер может воспроизвести доказательство в демонстрационном режиме.

Программа ТеорМат не предусматривает жесткого сценария доказательства, любое корректное доказательство приемлемо. Поэтому изучение математического анализа с помощью программы ТеорМат носит творческий характер.

Программа ТеорМат имеет обширную базу доказанных математических утверждений, содержащую все основные теоремы и многие теоретические задачи, изучаемые в МФТИ в темах "предел последовательности", "предел и непрерывность функции".

Программа ТеорМат может быть использована студентами для самостоятельной тренировки навыков доказательства теорем, а также преподавателями при проведении зачетов и коллоквиумов. С помощью программы ТеорМат в октябре 2002 года в МФТИ была проведена студенческая олимпиада по доказательству теорем с помощью компьютера.

Программа ТеорМат разрабатывается преподавателями кафедры высшей математики Московского физико-технического института. Автор алгоритмической части программы - Григорий Евгеньевич Иванов, автор интерфейсной части программы - Роман Викторович Константинов. © ТеорМат. 2000-2003.

Версию 3.0 программы ТеорМат можно бесплатно получить на сайте кафедры http://math.fizteh.ru/teormat. Эта версия не требует регистрации до 10 января 2004 года. Для работы с программой ТеорМат достаточно распаковать TeorMat.zip и запустить TeorMat.exe.

Кафедра высшей математики МФТИ проводит конкурс пользователей программы ТеорМат. При подведении итогов конкурса будет учитываться количество и сложность решенных задач и новых способов доказательств теорем, красота, краткость и оригинальность доказательств. Для участия в конкурсе следует директорию Protocols, в которой содержатся протоколы доказательств пользователя, поместить в архив, сохраняя пути к файлам. Полученный архив следует прислать по адресу theormath@mail.ru до 10 ноября 2003 года. В письме следует указать тему "конкурс-2003", а также фамилию, имя и координаты автора присылаемых доказательств.

Разработчики программы ТеорМат приглашают к сотрудничеству всех заинтересованных лиц. Предметом сотрудничества может быть, например,

• формулировка и доказательство математических утверждений, не содержащихся в базе ТеорМат;
• поиск и устранение ошибок;
• совершенствование алгоритмов и интерфейса программы ТеорМат;
• построение обучающих и проверяющих систем, теория и практика формальных доказательств, искусственный интеллект.

Отзывы, замечания и предложения направляйте по адресу theormath@mail.ru.