Выполнил: Маховиков В.А. Руководитель: Руденок А.Е.
Алгоритмический метод проверки справедливости утверждений общего характера в евклидовой геометрии полезен в области искусственного интеллекта и геометрического моделирования, так как используется при создании программ проверки существования гипотетических связей между геометрическими объектами на плоскости.
Цель– показать, как методы компьютерной алгебры могут помочь в доказательстве теорем планиметрии. Задача - – изучить методы автоматического доказательтсва теорем и применить их на практике.
Предметом изучения является метод компьютерной алгребры автоматического доказательства теорем планиметрии.
Условия и заключения геометрической теоремы задаются полиномиальными уравнениями от координат точек, о которых говорится в формулировке утверждения. Примечание: Не всегда есть возможность это сделать.
Геометрические утверждения, выводимые из предположений, представляются полиномами из идеала, порожденного предположениями
Принадлежность полинома радикалу проверяется алгоритмически за конечное число шагов.
Применение метода базисов Гребнера для решения конкретной здачи планиметрии.
Вычисления проводились в достаточно мощном пакете компьютерной алгебры Mathematica.
Алгебраические многообразия в работе использованы для автоматического доказательства теоремы. Такой же метод может быть использован для решения прямой и обратной задач робототехники для некоторых типов роботов.