Выпускная работа по «Основам информационных технологий» Магистрант кафедры диференциальных уравнеинй

Скачать 211.06 Kb.

Дата	03.10.2016
Размер	211.06 Kb.

БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Выпускная работа по

«Основам информационных технологий»

Магистрант

кафедры диференциальных уравнеинй

Маховиков Валерий

Руководители:

доцент Руденок Александр Евгеньевич,

старший преподаватель

Кожич Павел Павлович

Минск – 2009 г.

Список обозначений ко всей выпускной работе

ИТ - информационные технологи

- соноправленность

- многообразие

- идеал многообразия

- радикал идеала

k - кольцо полиномов

Реферат на тему «Применение ИТ в автоматическом доказательстве геометрических теорем»

Введение

Геометрическое описание робота и его движения используется управляющей программой для планирования его движений с целью выполнить требуемую задачу. Управляющая программа «размышляет» о геометрических ограничениях, связанных как с конструкцией робота, так и с условиями его работы, и «находит» подходящее решение задачи движения. Мы рассмотрим близкую задачу - автоматизация геометрических рассуждений, а также алгоритмический метод проверки справедливости утверждений общего характера в евклидовой геометрии. Этот метод полезен в области искусственного интеллекта и геометрического моделирования, так как используется при создании программ проверки существования гипотетических связей между геометрическими объектами на плоскости или теорем о них. Существует мнение, что такие программы демонстрируют понимание смысла геометрических утверждений, сравнимое с пониманием ученого-геометра. На самом деле вопрос о способности компьютера к интеллектуальному поведению совершенно неясен. Тем не менее, интересно отметить, что несколько новых (т.е. до сих пор неизвестных) теорем было доказано этими методами. В некотором ограниченном смысле, эти «доказыватели теорем» способны «размышлять» о геометрических конструкциях, т.е. делать то, что раньше считали уделом лишь человеческого разума.

Обзор литературы. Цели и задачи работы.

Алгоритмы, превращающие базовые понятия коммутативной алгебры и алгебраической геометрии из абстрактно-теоритических в конкретно-вычисляемые, стали бурно развивающейся научной областью. Обсуждение алгоритмов основывается на обобщении алгоритма деления для полиномов от одной переменной, найденом лишь в 60-х годах. Эти алгоритмы в соединении с мощьностью быстрых компьютеров привели к некоторым интересным приложениям – например, в робототехнике и доказательстве геометрических теорем.

Использование роботов позволяет облегчить или вовсе заменить человеческий труд на производстве, в строительстве, при работе с тяжёлыми грузами, вредными материалами, а также в других тяжёлых или небезопасных для человека условиях. Разработка алгаритмов поведения робота остается тяжелой задачей и предоставляет обширное поле для научной деятельности.

Цель работы – показать, как методы компьютерной алгебры могут помочь в доказательстве теорем планиметрии; обозначить место ИТ в решении этой проблемы.

Задача – изучить методы автоматического доказательтсва теорем и применить их на практике.

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

Во второй части реферата изложены результаты исследования примененные на практике при помощи ИТ, приложен программный код, описание.

Методология перевода геометрических теорем на язык алгебры и их доказательство.

Перевод геометрических теорем на язык алгебры.

Основа этого метода состоит в том, что, как только заданы декартовы координаты на евклидовой плоскости, условия, а также заключения некоторых геометрических теорем могут быть заданы полиномиальными уравнениями от координат тех точек, о которых говорится в формулировках соответствующих утверждений. Вот простой пример. Пусть A,B,C,D - вершины параллелограмма, представленного на рисунке.

Общеизвестная теорема утверждает, что диагонали и в точке пересечения N делятся пополам. Другими словами, AN=ND и BN=NC, где через XY мы обозначим длину сегмента , соединяющего точки X и Y. Стандартное доказательство использует равенство треугольников и . Чтобы установить связь этой теоремы с алгебраической геометрией, покажем, как конфигурация параллелограмма и его диагоналей (условия теоремы), а также утверждение, что точка N делит диагонали пополам (заключение теоремы), могут быть записаны в полиномиальной форме.

Свойства параллелограмма не зависят от сдвигов и поворотов плоскости. Значит, сдвигами и поворотами можно придать параллелограмму желательное положение, или, что эквивалентно, выбрать систему координат удобным образом. Проще всего сделать это так: точку A помещаем в начало координат, а сторону совмещаем с горизонтальной осью. Другими словами, A=(0,0), а B=(,0) для некоторого . Рассмотрим как неизвестную или переменную, значения которой могут быть выбраны произвольно в множестве R/{0}. Точка С имеет координаты (), где – новые переменные, не зависящие от . Координаты точки D полностью определены координатами точек A, B, C. При построении геометрической конфигурации, описываемой теоремой, координаты некоторых точек будут произвольными, тогда как координаты остальных точек будут определены (с точностью до конечного числа возможностей) значениями «произвольных» координат. Произвольные координаты будут обозначаться через , а другие координаты – через . Следует отметить, что разделение координат на два подмножества не задается однозначно условиями задачи. Различные способы описания одной и той же конфигурации приводят к различным полиномиальным формулировкам условий теоремы.

Так как D определяется точками A,B,C, то запишем D=(). Одним из условий теоремы является то, что четырехугольник ABCD – параллелограмм, т.е. его противоположные стороны параллельны, а следовательно, имеют одинаковые углы с осью абсцисс. Имеем:
0=,

=.
Освобождаясь от знаменателей, переходим к полиномиальным уравнениям

(1)
Теперь мы должны построить точку пересечения диагоналей. Так как координаты этой точки N определены координатами вершин, то N=. Утверждение, что N является пересечением диагоналей, означает, что N принадлежит и прямой , и прямой . Другими словами, тройки A,N,D и B,N,C коллинеарны. Это дает следующее соотношения:
A, N, D коллинеарны: ,

B, N, C коллинеарны: .

Освобождаясь от знаменателей, переходим к полиномиальным уравнениям

(2)
Система уравнений, составленная из уравнений (1) и (2), и является переводом условий теоремы на язык полиномов. Заключения теоремы могут быть также записаны в полиномиальном виде (с помощью теоремы Пифагора):
AN=ND:

BN=NC:

Упрощая эти выражения, перепишем эти утверждения в следующем виде:

=

= . (3)
Алгебраическая формулировка теоремы такова: если выполнены условия (1) и (2), то (3) также имеет место.

Ранее отмечалось, что можно различными способами перевести условия и заключения теоремы на язык полиномов. Например, способ, которым мы описали, что ABDC – параллелограмм, в виде уравнений (1), есть демонстрация того, как компьютерная программа могла бы формализовать тот факт, что . Другой метод перевода может использовать то, что D есть просто сумма векторов B=(,0) и C=(). Тогда в этой формализации (напомним, что D=())

(4)
Уравнения (4) значительно проще уравнений (1). Если хотим создать доказыватель геометрических теорем, который умел бы давать формулировку «ABDC-параллелограмм» непосредственно (т.е. не делая дополнительной редукции к виду « и »), то (4), конечно предпочтительнее (1). Далее, можно использовать для исключения переменной из условий и заключений, что даст более простую систему уравнений. В реальных задачах, связанных со сложными геометрическими конструкциями, такие геометрические упрощения могут быть просто необходимы.

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

Предложение: Пусть A, B, C, D, E, F-точки плоскости. Каждое следующее утверждение может быть записано в виде одного или нескольких полиномиальных уравнений:

параллелен ;
перпендикулярен ;
A,B,C коллинеарны;
Расстояние от A до B равно расстоянию от C до D: AB=CD;
C лежит на окружности с центром в A радиуса AB;
C середина отрезка ;
Острый угол равен острому углу :
делит пополам угол .

Доказательство: Метод перевода утверждений (i), (iii), (iv) на язык полиномов рассмотрен в предыдущем прмере. Утверждение (v) эквивалентно утверждению AC=CB. Утверждение (vi) есть конъюнкция двух утверждений: A, B, C коллинеарны и AC=CB. Утверждение (ii) переводится на язык полиномов через скалярное произведение векторов (). Утверждение (vii) эквивалентно тому, что =. Утверждение (viii) эквивалентно доказательству пункта (vii).

Определение. Геометрическую теорему назовем допустимой, если и ее условия, и ее заключения могут быть сформулированы на языке полиномов. Каждая допустимая теорема имеет множество алгебраических формулировок: перевод всегда неоднозначен.

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

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

Метод алгебраического доказательства геометрических теорем.

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

, …,= 0. (9)
Заключения теоремы также представлены полиномами от , . Достаточно рассмотреть случай одного заключения, потому что в противном случае можно рассматривать их по очереди. Запишем заключение в следующем виде:
, …,= 0.
Теперь вопрос можно сформулировать так: как тот факт, что следует из , …, может быть доказан алгебраически? Основная идея состоит в том, что должен обращаться в нуль там, где равны нулю полиномы ,…,.
Определение. Многообразие
(, …,) = {x ∈ : для всех ∈ }
определяет точки пространства, на которых обращаются в нуль все поли-номы из идеала, порождённого набором полиномов ,…,.
Определение. Пусть ,…, полиномы в. Положим
= { ∈}
,…,.
Определение. Идеал многообразия
= {∈ = 0 для всех ∈ }
порождается всеми полиномами, обращающимися в нуль на многообразии .
Обратим внимание, что уравнения (9) определяют многообразие
=(, …,)
Это наблюдение приводит к следующему определению:
Определение. Утверждение g называется строго следующим из условий

, …,, если , …,, где =(, …,).
Это определение кажется разумным, хотя ниже будет показано, что оно слишком «жесткое». В большинстве геометрических теорем встречаются «вырожденные» случаи, которые в данном определении не учитываются. Но пока будем использовать введенное выше понятие «строго следования».
Определение. Обозначим радикал идеала , который определяется следующим cоотношением:
= { : ∈ для некоторого ∈ N}.
Одним из недостатков определения «строго следования» является то, что нет эффективного метода нахождения , поскольку работаем над пространством Однако существует следующий критерий:
Предложение. Если , то строго следует из , …,.
Обратим внимание, что обратное утверждение неверно, если идеал строго содержится в идеале , что вполне возможно над . Тем не менее, предложение полезно, потому что условие может быть проверено с помощью алгоритма принадлежности радикалу.
Определение. Базис Грёбнера некоторого идеала алгебры многочленов относительно порядка

мультипликативность:
минимальность единицы: 1 0.

Определение. Редуцированным базисом Гребнера полиномиального идеала, называется его базис Гребера , такой что

все старшие коэфициенты равны 1 для любого
никакой моном никакого не принадлежит идеалу старших мономов множества .

Теорема: Пусть =, …,. Тогда

{1}
является редуцированным базисом Гребнера для .
Если это условие выполнено, то строго следует из , …,.

Предложение. обобщенно следует из условий , …,, если существует ненулевой полином с(), такой что с, где H=, …,.
Следствие. В условиях предложения «обобщенного следствия» следующие утверждения эквивалентны:

существует ненулевой полином с(), такой что с
{1} является редуцированным базисом Гребнера идеала , …,.

Объединяя п. (ii) с предложением, получаем алгоритмический метод доказательства того, что заключение теоремы обобщенно следует из ее условий. Назовем этот подход методом базисов Гребнера в доказательстве геометрических теорем.

Системы компьютерной алгебры.

Для решения задач, связанных с нахождением базиса Гребнера, могут использоваться следующие программы: AXIOM, Maple, Mathematica, REDUCE, Singular. Все они представляют собой достаточно мощные пакеты программ.

Я использововал в своей работе пакет Mathematica. Эта программа имеет хорошие возможности для вычисления базисов Гребнера. Система не содержит специального пакета для вычисления - основные команды являются частью ее ядра.

Mathematica знает все мономиальные упорядочения. Наиболее важными командами являются PolynomialReduce и GroebnerBasis. Эти команды вычисляют остаток и частные от деления некоторого полинома на полиномы из списка, используя мономаильное упорядочение, и, соответсвенно, вычисляют базис Гребнера.

Полезными командами являются также:

MonomialList, которая генерирует список членов полинома в соответсвии с заданным упорядочением.
Eleminate, которая исключает переменные из системы полиномиальных уравнений.
Solve, находящая все решения системы.

Более полную информацию о возможностях пакетов можно найти в документациях и мануалах. Использование таких программ делает возможным поиск решения сложных задач.

Данная ссылка указыает на сравнение систем компьютерной алгебры: http://en.wikipedia.org/wiki/Comparison_of_computer_algebra_systems

Результаты исследования на практике.

В этой части мы применим полученые знания на практике для доказательства геометрической теоремы методом базисов Гребнера. Пример покажет опыт реализации ИТ в исследованиях. Будут приложены программные коды и описание.

Вычисления проводятся в пакете Mathematica.
Задача. В треугольнике ABC проведена медиана . На медиане произвольно взята точка P. Через точку P до пересечения с прямыми BC и AC проведены прямые и . Докажите, что .

Решение. Поместим начало координат в точку A. Тогда точка A имеет координаты (0,0), C-(,0), а B-(,). -точка пересечения медианы со стороной AB, имеет координаты (,).-произвольная точка медианы с координатами (,). и имеют соответственно координаты (,) и (,0).Тогда, условия теоремы имеют вида:
-середина AB: =2-,

-середина AB: =2-,

C, P, коллинеарные: ,

B,, C коллинеарные: ,

A, P, коллинеарные:

B, P, коллинеарные: .
Заключение g имеет вид:
g=.
Тогда, вычислив базис Гребнера идеала , мы не получаем {1}. Вычислим базис Гребнера идеала .
Получаем:
GroebnerBasis[{h1, h2, h3, h4, h5, h6}, {x1, x2, x3, x4, x5, x6, u1, u2, u3}]

Разлагая идеал на 2 компоненты и отбрасывая ту компоненту, на которой обращается в нуль, и, вычисляя повторно базис Гребнера, мы получаем:

Продолжая данный процесс, мы получаем следующие базисы:

3 шаг:

4 шаг:

5 шаг:

6 шаг:

7 шаг:

Вычислив редуцированный базис Гребнера, мы получаем {1}, а значит, теорема доказана.
Таким образом, при помощи пакета Mathematica, в этой части мы смогли доказать геометрическое утверждение, основываясь на методе базисов Гребнера.

Заключение.

Решение многих задач коммутативной алгебры до недавнего времени было невозможно. С развитием ИТ эта сфера научной деятельности стала быстро развиваться.

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

Результатом работы стало доказательство геометрического утверждения на конкретном примере с использованием информационных технологий: пакета Mathematica.

Описанный метод в совокупности с использованием компьютерых программ позволяет доказать широкий спектр утверждений и теорем. Некоторые новые теоремы были доказаны на его основе.

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

Список литературы к реферату.

М. Атья, И. Макдональд. Введение в коммутативную алгебру. М., Факториал Пресс, 2003.
D. Eisenbud. Commutative Algebra with a View toward Algebraic Geometry. Springer.
Д. Кокс, Дж. Литтл, Д. О'Ши. Идеалы, многообразия и алгоритмы. Введение в вычислительные аспекты алгебраической геометрии и коммутативной алгебры. М., Мир, 2000.
И. В. Аржанцев. Системы алгебраических уравнений и базисы Грёбнера. М., МАКС Пресс, 2002. Е. В. Панкратьев. Элементы компьютерной алгебры. М., БИНОМ. Лаборатория знаний. 2007.
В. В. Прасолов. Многочлены. М., МЦНМО, 2001.
M. Kreuzer and L. Robbiano. Computational Commutative Algebra, volumes 1 and 2, 2000.
Mathematica, Wolfram, 1996.

Предметный указатель к реферату.

Б
базис Гребнера 10

- редуцированный базис Гребнера 11
Д
допустимая теорема 8
И
идеал многообразия 10

M
многообразие 9

метод базисов Гребнера 11
Р
радикал 10
У
утверждение

- строго следующее 10

- обобщенно следующее 11

Интернет ресурсы в предметной области исследования.

http://wikipedia.org – свободная общедоступная многоязычная универсальная энциклопедия;

http://www.emis.de/journals/FPM/ps/k03/k033/k03315.pdf - статья посвященная автоматическому доказательству геометрических теорем методом базисов Гребнера;

http://www.wolframalpha.com/index.html - библиотека систематизиро-ванных знаний;

http://google.com – первая по популярности в мире поисковая система;

http://wolfram.com/ - сайт создателей Mathematica на котором можно

купить программу и изучить документацию.

http://window.edu.ru/ –образовательные ресурсы; Множество статей по всем сферам образования.

Действующий личный сайт в WWW.

http://makhavikou.narod.ru/

Граф научных интересов.

Магистрант ММФ Маховиков В.А.

Специальность - компьютерная математика

Смежные специальности

01.01.01 – математический анализ

1.Анализ на многообразиях, p-адический анализ, нестандартный анализ, различные направления конструктивного анализа, интервальный анализ, анализ в упорядоченных пространствах.

2. Абстрактные и функциональные пространства, наделенные алгебраическими, топологическими, метрическими, порядковыми и др. структурами. Измеримые пространства.

01.01.04 – геометрия и топология

Основания геометрии, псевдоевклидова и неевклидова геометрия, дискретная геометрия, аффинная геометрия, проективная и другие геометрии, геометрия над произвольными алгебрами, теория выпуклых множеств, исследование геометрических фигур и геометрических неравенств, дискриптивная геометрия, локальная и глобальная дифференциальная геометрия классических пространств, терия гладких многообразий и подмногообразий и связанных с ними дифференциально-геометрических структур;

Основная специальность

01.01.06 – математическая логика, алгебра и теория чисел

Теории полугрупп, групп, колец, модулей и алгебр, полей и многочленов; линейная и полилинейная алгебра, гомологическая алгебра и алгебраическая K-теория; алгебраическая геометрия, топологическая алгебра; теории категорий, т структур и универсальных алгебр.

Сопутствующие специальности

01.04.02 – теоретическая физика

1. Математические методы теоретической физики (развитие и применение теории операторов, алгебр, групп и их представлений, геометро-топологических подходов).

2. Классическая (релятивистская и нерелятивистская) механика, включая, статистическую.

01.02.04 – механика деформируемого твердого тела

Моделирование биомеханических систем на основе моделей деформируемых сред.

Тестовые вопросы по Основам информационных технологий.

Тег используется для:

загрузки и отображения объектов (например, видеофайлов, флэш-роликов, некоторых звуковых файлов и т.д.), которые исходно браузер не понимает;
служит контейнером для элементов , которые определяют активные области для карт-изображений;
устанавливает маркированный список;
помечает текст как цитату или сноску на другой материал;

Команда, которая генерирует список членов полиномов в соответсвии с заданным упорядочением в пакете Mathematica:

MonomialList
PolynomialReduce
Eliminate
GroebnerBasis

Презентация магистерской диссертации.

http://makhavikou.narod.ru/Presentation.ppt

Список литературы к выпускной работе.

М. Атья, И. Макдональд. Введение в коммутативную алгебру. М., Факториал Пресс, 2003.
D. Eisenbud. Commutative Algebra with a View toward Algebraic Geometry. Springer.
Д. Кокс, Дж. Литтл, Д. О'Ши. Идеалы, многообразия и алгоритмы. Введение в вычислительные аспекты алгебраической геометрии и коммутативной алгебры. М., Мир, 2000.
И. В. Аржанцев. Системы алгебраических уравнений и базисы Грёбнера. М., МАКС Пресс, 2002. Е. В. Панкратьев. Элементы компьютерной алгебры. М., БИНОМ. Лаборатория знаний. 2007.
В. В. Прасолов. Многочлены. М., МЦНМО, 2001.
M. Kreuzer and L. Robbiano. Computational Commutative Algebra, volumes 1 and 2, 2000.
Mathematica, Wolfram, 1996.
M. Kreuzer and L. Robbiano. Computational Commutative Algebra, volumes 1 and 2, 2000.
Брайан Пфаффенбергер, Стивен Шафер, Чак Уайт, Билл Кароу. HTML и CSS. Библия пользователя.
Н. Д. Льюис. Word, Excel, PowerPoint, Outlook. Наглядный самоучи-тель.

Приложения

База данных защищена авторским правом ©infoeto.ru 2022
обратиться к администрации
Как написать курсовую работу | Как написать хороший реферат