Выполнил: Маховиков В.А. Руководитель: Руденок А.Е. - презентация

1 Выполнил: Маховиков В.А. Руководитель: Руденок А.Е.

2 Алгоритмический метод проверки справедливости утверждений общего характера в евклидовой геометрии полезен в области искусственного интеллекта и геометрического моделирования, так как используется при создании программ проверки существования гипотетических связей между геометрическими объектами на плоскости.

3 Цель– показать, как методы компьютерной алгебры могут помочь в доказательстве теорем планиметрии. Задача - – изучить методы автоматического доказательтсва теорем и применить их на практике.

4 Предметом изучения является метод компьютерной алгребры автоматического доказательства теорем планиметрии.

5 Условия и заключения геометрической теоремы задаются полиномиальными уравнениями от координат точек, о которых говорится в формулировке утверждения. Примечание: Не всегда есть возможность это сделать.

6 Геометрические утверждения, выводимые из предположений, представляются полиномами из идеала, порожденного предположениями

7 Принадлежность полинома радикалу проверяется алгоритмически за конечное число шагов.

8 Применение метода базисов Гребнера для решения конкретной здачи планиметрии.

9 Вычисления проводились в достаточно мощном пакете компьютерной алгебры Mathematica.

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

11