Cuando solía competir en la Olimpiada de Competiciones de vuelta en la escuela secundaria, un número decente de los más fáciles de geometría cuestiones se pueden resolver a través de lo que llama una geometría de bash. Básicamente, tendría que etiquetar cada ángulo en el diagrama de la variable, a continuación, utilizar un conjunto limitado de la geometría básica de las operaciones para encontrar las relaciones entre los elementos, eliminar ecuaciones y, a continuación, usted había, finalmente, obtener el resultado. Parece ser el tipo de cosa que usted podría programar un ordenador para hacer. Así, tengo curiosidad, ¿existe algún software para hacer esto? Sé que hay un montón de software para la resolución de ecuaciones, pero hay algo que en realidad le permite la entrada de una geometría del problema sin la conversión manual de ecuaciones? Yo no estoy buscando nada demasiado adelantado, incluso viendo un intento de ser una opción interesante. Si hay algo decente, creo que sería bastante interesante para ejecutar los resultados en los diversos concursos y ver cómo muchas de las preguntas que se resuelve.
Respuestas
¿Demasiados anuncios?
Este es sólo un caso especial de los sistemas automatizados de teoremas. Una cosa buena es que algunos geometría del problema de hecho puede ser resuelto por un algoritmo.
Hay teorías muestran tal sistema puede ser observado a través de algoritmos. No sé si alguien tiene realmente escribió el programa para hacerlo. JGEX parece que no.
Un mecánico de la geometría de la prueba técnica fue popularizada en China por Jingzhong Zhang. Él introdujo por primera vez como una forma de máquinas para resolver problemas geométricos relativos a las proporciones entre las áreas, longitudes o ángulos. A continuación, algunos Olimpiada de la gente que conozco empezar a usarlo para bash que tipo de problema. No sé cuál es el nombre está en inglés, pero la traducción literal de el método es el "punto de método de eliminación". Aunque no es exactamente igual a lo que usted está hablando, porque "a la entrada de la geometría del problema" requiere que usted provea la construcción del problema desde un borde recto y un compás, que es casi como el "manual de conversión a la de las ecuaciones".
la idea básica:
Construir el problema original por compás y una regla, haga una lista de todos los construidos punto ordenadas por el orden de la construcción, que sea la L. Registro de los puntos que se utilizan en la construcción de cada punto.(Sólo los puntos utilizados para la construcción de un punto P son utilizados en la sustitución de los pasos 3 y 4)
Traducir el teorema en una forma equivalente. Generalmente a/b = 1, donde a y b son funciones de la longitud y el área de determinados segmentos o triángulos. Vamos a llamar a esta ecuación E.
Sea P el último punto de L. Para cada P aparece en el Correo, sustituirlo con otra relación con el uso de otros puntos de L(P sí también está permitido), por lo general, si estamos probando acerca de longitudes, podemos utilizar la zona. Una lista de posibles operaciones son necesarias para este paso. Puede ramas como una prueba de árbol cuando el programa de decidir el uso de diferentes sustituciones.
Hacer otra sustitución que elimina el punto P. Por ejemplo, si en el paso anterior, se sustituye la longitud de la zona, entonces queremos encontrar algo que implican la longitud.
Hacer de 3 a 4 más y más hasta que tenemos 1=1
Un ejemplo:
Teorema de la bisectriz de un ángulo
Dado: $AD$ es la bisectriz de un ángulo de $\angle BAC$ de triángulo $\triangle ABC$. Deje $XYZ$ ser el área del triángulo $\triangle XYZ$, e $XY$ ser la longitud del segmento de $XY$.
Probar: $\frac{AB}{AC} = \frac{BD}{DC}$
Prueba:
En primer lugar, construir $ABC$. A continuación, construir $AD$. Los puntos en la lista de $L$$A,B,C,D$.
La ecuación equivalente al teorema es $\frac{AB}{AC} \frac{DC}{BD} = 1$
$\frac{AB}{AC} \frac{DC}{BD} = \frac{AB}{AC} \frac{ACD}{ABD}$ (sustituto de la longitud de la zona)
$=\frac{AB}{AC} \frac{\frac{1}{2} AC\cdot AD \sin \angle CAD}{\frac{1}{2} AB\cdot AD \sin \angle BAD}$, este paso con éxito eliminar el punto de $D$ por cancelación.
$=\frac{AB}{AC} \frac{AC}{AB} =1$
Este es sólo un no-formal explicación de cómo automatizado sistema de trabajo. Creo que el siguiente libro de Zhang le dirá más acerca de él: la Máquina de pruebas en geometría: la producción automatizada de los legible pruebas de los teoremas de la geometría. No he leído el libro, pero la descripción de parece que lo que usted está buscando. Un par de papel por Zhang y su colega se pueden encontrar en la JGEX del sitio web. El JGEX documentación es automático teorema de armario es también un gran recurso.
Usted podría estar interesado en la Página Web de Doron Zeilberger. Él tiene una página titulada "geometría plana: un libro de texto elemental (Circa 2050)" donde él imaginó un mundo en el que equipos pueden derivar de geometría plana sin interferencia o intervención humana. El paquete de Maple que demuestra muchas declaraciones por la computadora.
La página existe en http://www.math.rutgers.edu/~zeilberg/PG/gt.html.
