2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 Mechanical Geometry Theorem Proving
Сообщение14.09.2013, 13:21 
В этой теме предлагается обсуждать различные вопросы, относящиеся к доказательству теорем геометрии методами компьютерной алгебры. Прилагаю препринт моей статьи "О механическом доказательстве планиметрических теорем рационального типа" (журнал "Программирование", 2013). Было бы интересно увидеть замечания, комментарии и т.п. по теме статьи.

Аннотация. В статье предлагается элементарный подход к механическому доказательству планиметрических теорем рационального типа. Это подход реализован в виде программных модулей geom и его модифицированной версии geom_zeta, созданных в системе компьютерной алгебры Maple. Приводятся многочисленные примеры механических доказательств сложных теорем планиметрии (как хорошо известных, так и сравнительно новых) на основе удобных рациональных параметризаций.

Ниже приводятся ссылки на некоторые темы форума, где можно увидеть примеры механического доказательства теорем планиметрии:

Диагонали вписанного шестиугольника
Треугольник и три центра описанных окружностей
Орбиты Жукова
Подобные равнобедренные треугольники
Обсуждение и разбор марафонских задач-ММ157
Задача на построение
Очень сложная геометрическая задача
Гипотеза о трёх параболах


У вас нет доступа для просмотра вложений в этом сообщении.

 
 
 
 Re: Mechanical Geometry Theorem Proving
Сообщение18.09.2013, 19:43 
Вот ещё несколько текстов (файлы Mechanical-Geometry-Theorem-Proving-1.pdf, Mechanical-Geometry-Theorem-Proving-2.pdf, theorem-about-incenters.pdf) с многочисленными примерами механического доказательства (решения) планиметрических теорем (задач). Эти тексты более элементарны и вполне доступны школьникам.


У вас нет доступа для просмотра вложений в этом сообщении.

 
 
 
 Re: Mechanical Geometry Theorem Proving
Сообщение22.09.2013, 09:43 
Вот пример задачи рационального типа с "внешними" условиями (выделено жирным шрифтом).

В треугольнике $ABC$ с углом $\angle BAC=60^\circ$ проведена биссектриса $BD$ и затем продолжена до пересечения в точке $S$ с описанной окружностью. Пусть $K$ --- вторая точка пересечения прямой $AB$ с окружностью, описанной около треугольника $ADS$. Найдите $|BC|$, если $|AB|=8$ и $|AK|=1$.

Чтобы решить эту задачу механически, сначала переформулируем её: будем искать $|BC|/|AK|$ при условии $|AB|/|AK|=8$. Далее можно применить $T_aT_bT_c$-параметризацию: $T_a=z_1$, $T_b=1$, $T_c=\zeta=\cos{120^\circ}+i\sin{120^\circ}$. Следующие вычисления проделаны с помощью модуля geom_zeta:
$$
A=2\eta^2, \quad B=\frac{2(\eta^2-1)z_1}{z_1-1+\eta^2}, \quad C=\frac{2z_1}{z_1+1}, \quad D=\frac{2z_1}{z_1-\eta^2}, \quad O=\frac{2\eta^2z_1(z_1+\eta^2)}{(z_1-1+\eta^2)(z_1+1)}, \quad S=\frac{2\eta^2z_1}{z_1+1},
$$
$$
O_1=\frac{2\eta^2z_1(z_1+1-\eta^2)}{(z_1-\eta^2)(z_1+1)}, \quad K=\frac{2(\eta^2-1)z_1}{z_1+1}
$$
($O$ и $O_1$ --- центры описанных окружностей треугольников $ABC$ и $ADS$ соответственно). Теперь имеем $|AB|^2/|AK|^2-64=f(z_1)/g(z_1)$, где
$$
f(z_1)=441z_1^4+(-896+1792\eta^2)z_1^3-2226z_1^2+(896-1792\eta^2)z_1+441.
$$
Осталось вычислить
$$
a=\frac{|BC|^2}{|AK|^2}=-\frac{3z_1^2}{(z_1-1+\eta^2)^2(z_1+\eta^2)^2}
$$
при условии $f(z_1)=0$. Пусть $h(z_1)$ --- числитель дроби $|BC|^2/|AK|^2-a$. Результант многочленов $f(z_1)$ и $h(z_1)$ равен $194481(a-49)^2(a-81)^2$. Таким образом, $a=49$ или $a=81$. Отсюда ответ к задаче: $|BC|=7$ или $|BC|=9$ (можно показать, что оба варианта реализуются).

 
 
 
 Re: Mechanical Geometry Theorem Proving
Сообщение28.09.2013, 17:40 
Вот ещё один пример теоремы с "внешним" условием (на это раз условие имеет вид равенства с дополнительными ограничениями типа неравенств, т.е. по существу не является алгебраическим).

Если в треугольнике $ABC$ две чевианы $BB_1$ и $CC_1$ равны, а их точка пересечения лежит на биссектрисе угла при вершине $A$, то треугольник $ABC$ --- равнобедренный.

Пусть $A=0$, а $P=1$ --- общая точка чевиан $BB_1$ и $CC_1$. Положим $C=bz_1$, $B=cz_1^{-1}$, где $z_1+z_1^{-1}=2\cos{\phi}>0$. Тогда
$$
B_1=\frac{cz_1^2}{cz_1^2-z_1+c}, \quad C_1=\frac{b}{bz_1^2-z_1+b}, \quad Q=\frac{bc(z_1^2+1)}{(b+c)z_1},
$$
где $Q>1$ --- основание биссектрисы. Вычислив $|BB_1|^2-|CC_1|^2$ и приравняв к нулю, мы получим либо $b=c$ (что нам и нужно), либо $z_1^2bc-bz_1+bc-cz_1=0$ (что равносильно равенству $Q=1$ и потому невозможно), либо
$$
4bc\cos{\phi}+\frac{b^2+c^2+1}{\cos{\phi}}=2(b+c)(bc+1).
\eqno(*)
$$
Последнее равенство также невозможно. Действительно, из неравенства $Q>1$ следует, что
$$
1>\cos{\phi}>\frac{b+c}{2bc}.
\eqno(**)
$$
Отсюда $2bc>b+c$ и, как следствие, $b+c>1$. На интервале $(**)$ левая часть $(*)$ как функция $\cos{\phi}$ является выпуклой и, как нетрудно убедиться, на концах этого интервала меньше правой части. Поэтому левая часть $(*)$ всюду меньше правой.

Геометрическое доказательство этой теоремы (обобщающей известную теорему Штейнера-Лемуса) см. в журнале "Математика в школе", 1948, № 1.

 
 
 [ Сообщений: 4 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group