СИСТЕМА ПОИСКА ДОКАЗАТЕЛЬСТВА ТЕОРЕМ ПЛАНИМЕТРИИ
Попов Сергей Викторович, Костин Виктор Сергеевич, Матунова Татьяна,
Московский инженерно физический институт (технический университет) (МИФИ), г. Москва
Рынок обучающих систем, предлагающий электронные версии учебников или задачников и увеличение парка домашних компьютеров, позволяет говорить о том, что школьник с успехом может получать знания не только в школе, но и дома. Современные обучающие системы подразумевают одностороннюю вовлеченность обучаемого в усвоение материала, так как могут передать ему только те знания, которые заложили в них разработчики, что не позволяет обучаемому развивать такие важные аспекты личности, как творчество и нестандартность мышления. Кроме этого, от того, что учебник или задачник стал электронным, он не изменился по содержанию и процесс изучения предмета не стал качественно другим.
Коллективом авторов была реализована система поиска доказательств планиметрических задач. Она отличается от уже существующих тем, что позволяет обучаемому активно участвовать в процессе усвоения знаний за счет выработки навыков решения новых, нестандартных задач.
В обучающих системах можно выделить две основные составляющие: интеллектуальную часть (т.е. систему поддержки поиска решения) и диалоговую подсистему. В существующих обучающих системах наблюдается явное преимущество интерфейса перед интеллектом.
Поддержка пользовательского интерфейса в предлагаемой системе представляет собой графический редактор, позволяющий вводить чертеж и осуществлять все необходимые преобразование чертежа, которые использует человек при описании условий геометрической задачи. Помимо графической части редактор содержит средства для описания всех соотношений между элементами чертежа и ввода конкретных значений параметров тех или иных элементов чертежа, средства формулирования заключение задачи или теоремы. Тем самым язык общения с системой ничем не отличаться от языка проблемной области (в данном случае - планиметрии).
Графическая часть системы непосредственно взаимодействует с ее интеллектуальной подсистемой, которая и отвечает за поиск решения.
В основе подсистемы поиска решения лежит метод логического моделирования построение неподвижной точки в классе нормальных моделей. Этот метод отличается от стандартных процедур поиска доказательств, например резолюционной, следующим. В методе резолюций пространство поиска мало чем напоминает действительную формулировку задачи, так как исходная задача переводится на язык дизъюнктов. А при поиске неподвижной точки строится логическая модель исходной задачи, которая соответствует естественному (человеческому) доказательству, так как отношения и функции языка, предназначенного для описания задачи, однозначно соответствуют ее естественно-языковой формулировке, и правила построения новых элементов доказательства напоминает способ построения человеком естественного доказательства. Когда же осуществляется переход в класс нормальных моделей, т.е. моделей, единицами которых являются не отдельные элементы, а классы эквивалентности, то преодолевается еще одно ограничение стандартных систем поиска доказательств - трудность работы с равенством.
Трудность реализации подобных интеллектуальных систем состоит в том, что современные средства программирования мало приспособлены для их написания, так как приходится одновременно описывать два процесса: порождения элементов доказательства и управление этим процессом. Поэтому для программирования интеллектуальной части используется т.н. двухуровневый язык ПОКОС: его нижний уровень базируется на механизме построения логических моделей и выводов и предназначен для порождения элементов доказательств, а верхний уровень представляет собой язык управления потоками данных. Разделяя процессы порождения и управления, удается существенно облегчить создание программ по решению задач переборного характера и снизить трудозатраты на реализацию подсистем поиска решения.
Предпринятая системой попытка автоматически найти доказательство или решение не всегда бывает успешной, т.к. во введенном условии задачи может не хватать некоторого дополнительного элемента, существенного для нахождения всего решения, или задача может быть введена не в полном объеме. В этом случае, после нахождения неподвижной точки, система поиска выдает сообщение, что задача не была решена и предоставляет возможность просмотреть все данные, которые были получены к этому моменту. Анализируя это незавершенное решение, учащийся выделяет те данные, которые, по его мнению, обеспечат возможность дальнейшего, более успешного поиска решения и на их основании решает какое дополнительное построение следует осуществить, чтобы получить окончательное решение или продвинуться вперед еще на один шаг в попытке решить задачу.
Таким образом, обучаемый полностью вовлечен в процесс поиска решения или доказательства. Он может сам планировать решение, разбивать задачу на подзадачи, выдвигать и проверять гипотезы, вводить дополнительные условия, ограничения, построения и т.п. Поэтому сеанс общения с системой почти ничем не отличается от обычной творческой деятельности по поиску неизвестного решения за исключением одного: компьютер не игнорирует ни одно предложения, терпеливо и подробно объясняя все возникающие варианты и анализируя предлагаемые способы решения.
Литература
![]() | Сервер поддерживается фирмой НПП "БИТ про" Лучшие программы для образовательного процесса |
|