La demostración automática de teoremas en Geometría elemental y su repercusión didáctica

OTROS TRABATOS LA DEMOSTRACION AUTOMATICA DE TEOREMAS EN GEOMETRIA ELEMENTAL Y SU REPERCUSION DIDACTICA MIRANDA DIAZ, 1. Escuela Universitaria de Formación del Profesorado de EGB. Universidad de Cantabria. Santander. SUMMARY The relevant role of validatory tasks in the traditional teaching of geometry is currently approached as a mere introduction to logical reasoning. The existence of automatic proof algorithms to any elementary geometry theorem and their recent implementation in computers gives a peculiar character to the kind of reasoning used in this theory -one of the few being decidibleand modifies its educational meaning. On the other hand, the analysis of the way of teaching geometry shows excessive emphasis on training by discovering models, neglecting the building up of theoretical bodies of knowledge. Both facts demand an exploration of new techniques in the teaching of geometric proofs; we describe and analyze the use of educative software (based on A.I. tecnhiques) for automatic proof programs now operating. 1. LA DEMOSTRACION AUTOMATICA DE TEOREMAS GEOMETRICOS En los últimos afios se han producido avances imporpuede ser grande: nos referimos a la implantación e intantes en un tema en el que se interrelacionan aspectos vestigación de diversos sistemas informáticos que reade matemática pura y de ciencias de la computación lizan demostración automática de teoremas en geomey cuya influencia en la ensefianza de las matemáticas tría elemental. ENSERANZA DE LAS CIENCIAS, 1988, 6 (11, 61-65 61 OTROS TRABAJOS Utilizando un lenguaje sencillo podríamos decir que el objetivo final de la demostración automática en geometría consiste en lograr que un ordenador, al que se k suministre una serie de hipótesis y una tesis, responda si dicha tesis es cierta o falsa; y, en caso afirmativo, suministre una demostración de dicha tesis. Este objetivo se aborda en la actualidad desde dos enfoques distintos, usando en ambos la ayuda de los ordenadores. El primer enfoque, que arranca en los trabajos de Tarski en la década de los 30 -sobre eliminación de cuantifi cadores-, consiste en traducir los enunciados geometricos, por medio de coordenadas, a fórmulas algebraicas. Esta traducción tiene que ser realizada previamente a la introducción de datos en la máquina. Se obtiene finalmente una expresión del tipo A =>B donde A y B son un conjunto de ecuaciones polinómicas, como en el ejemplo siguiente (Kutzler, B., Stifter, S., 1986), que describe la demostración del caso especial del teorema del círculo de Apolonio, «en un triángulo rectángulo el pie de la altura de la hipotenusa y los puntos medios de los tres lados están en una circunferencia». Consideramos ahora la siguiente formulación algebraica de las hipótesis de este problema. (R as punta medio de CA) hl = p - Y 3 1-O h2 = a4 - yl = O (P as punto -dio de AB) h3 = b5 - Y2 = 0 - (C es punte medio de BC) hg = - Y2 = O (longitud 81 long Fll) h5 = (y7 - Y31Z + Y; - (Y? - - (ya - yg12 = O (181lOn. Q) h6 Iy7 - y3)2 + y: - (y8 - y6)' -Y: = O (ti está en AB) h7 = (Y,, - yl) y2 + y1 Y10 0 (DH perpendicular a AB) h8 = -Yl Y,, + Y2 Y10 = O La temi. admite 1s siguiente foriulación: (lo,,,, Ell = lon. Hn) C = (y7 - y312 + Y; - (y7 - - - yl0+ = O Por tanto el teorema que se desea comprobar puede reducirse a verificar la verdad o falsedad de la siguiente expresión: A partir de esta Última expresión algebraica se pueden utilizar diversos algoritmos para decidir mecánicamente si la misma es verdadera o falsa. El primero de ellos -sólo de interés teóricose encuentra en los trabajos de Tarski antes mencionados; pero el tiempo que necesita para ser ejecutado en un ordenador lo hace impracticable aun para atacar pre blemas bastante sencillos. Por ello el primer algoritmo ejecutable efectivamente en un ordenador es el denominado de descomposicidn algebraica cilíndrica (CAD), debido a Collins y que ha sido implementado con las mejoras introducidas por Arnon y Mc Callum en un IBM 4341 en 1984. Este programa está en la actualidad disponible, con ciertas restricciones, para grupos de investigación que lo soliciten a sus autores; aunque en Espaiia aún no se posee. Debido a que el tiempo de ejecución de este programa CAD sigue siendo bastante elevado, se considera como un avance importante otro algoritmo, desarrollado por el profesor Wu Wen-Tsün en 1984, que permite demostrar automáticamente aquellos teoremas de geometría elemental en los que no se haga referencia a los axiomas de orden. Este algoritmo, aún no totalmente entendido desde el punto de vista teórico, tiene una menor complejidad operativa que los anteriores; implementado en un HP 1000 ha permitido recientemente la demostración automática de más de trescientos teoremas: Desargues, Simson, Ceva, círculo de los nueve puntos etc., en algunos segundos. Una bibliografía bastante completa de los algoritmos mencionados aquí aparece en Kapur, D. ((Geometry Theorem Proving using Hilbert's Nullstellensatz)). Proceed. SYMSAC 86. U. Waterloo. 1986. Este enfoque que estamos comentando se caracteriza porque, ante cualquier cuestión geométrica planteada al ordenador, éste ofrece siempre una respuesta afirmativa o negativa correcta; los pasos del algoritmo que ejecuta el ordenador constituyen la demostración o refutación de la cuestión; además puede programarse para que seiiale bajo qué hipótesis adicionales la cuestión es cierta. Por ejemplo: si planteamos como teorema que hay que probar que por tres puntos del plano pasa al menos una circunferencia, seiialaría que es necesario que no estén alineados para su verificación. Otro enfoque radicalemnte distinto para la demostración automática de teoremas geométricos utiliza los métodos de la inteligencia artificial. Aquí no se trata, hablando con cierta imprecisión, de que el ordenador utilice, como en el enfoque anterior, un algoritmo. En este caso los programas de demostración automática incluyen una base de conocimientos geométrico formada por una serie de axiomas y teoremas de la geometría elemental y unas reglas de inferencia proporcionadas a través de un lenguaje de programación lógica. Una vez propuesta una tesis a partir de unas hipótesis, el programa genera deducciones de las hipótesis usando la base de conocimientos; estas deducciones pueden ser o no apropiadas para conseguir la demostración de la tesis. De esta manera se obtiene un árbol de deduccioENSERANZA DE LAS CIENCIAS, 1988, 6 (1) OTROS TRABAJOS nes en cascada entre las que eventualmente se encuentra el objetivo propuesto; o bien, transcurrido cierto tiempo, el programa reconoce que no es capaz de hallar la demostración. A esta desc~ipción extremadamente simplista del comportamiento del demostrador automático en este segundo enfoque debemos afiadir que el programa contiene, además, una serie de estrategias heurísticas para encauzar la explosión combinatoria del árbol de deducciones (p. ej. consultando a la base de datos antes de iniciar una deducción, registrando procedimientos que no han tenido éxito en intentos precedentes, desarrollando el árbol de deducciones simultáneamente a partir de las hipótesis y también de las tesis, ajustando la búsqueda del objetivo en el árbol usando diversas técnicas, como las de examen en anchura o en profundidad, etc.). Un análisis más detallado del trabajo existente en este campo -usando el enfoque de la inteligencia artificial y comparando los distintos programaspuede consultarse en Coelho-Moniz (1986). Además podemos seAalar que en los últimos dos aAos se conocen experiencias concretas, aunque aún en una fase exploratoria, de utilización de estos mecanismos de demostración automática, usando PROLOG e implementados en micros (128 Kb), en la ensefianza de la geometría para alumnos del nivel de ensefianzas medias. Los trabajos de Anderson (1985), Giorgiutti (1986) y Hadzikadic, Lichtenberguer-Yun (1986) son un ejemplo de esto, aunque todavía con un escaso desarrollo de los aspectos de comunicación con el alumno (interface humana) que condujeran a situaciones de aprendizaje. Por ejemplo, en el programa GEOM elaborado por CoelhoMoniz, supongamos que el alumno se plantea la demostración o refutación del siguiente teorema geométrico: «la recta que une los puntos medios de las diagonales de un trapecio interseca a éste en los puntos medios de los lados no paralelos)), es decir Cuestión: M punto medio de AD (análogamente para la intersección de la recta EF con CB) Para ello el profesor introduce las siguientes hipótesis así como el objetivo, convenientemente codificados, en el demostrador de teoremas (o tal vez esta tarea es realizada por el propio alumno si conoce los códigos). Contexto (optativo) Datos . - rectas AKB Hipótesis AB // DC BC E punto medio de AC CD F punto medio de BD DM A AEC DFB MEF CFK Objetivo M es punto medio de AD La respuesta del ordenador en este caso es simplemente una colección de frases en inglés que describen escuetamente el procedimiento de demostración. GIVEN LINES: AKB. BC. CD. DMA. AEC, DFB, MEF. CPK GIMN A0 PARALLEL TO DC GIVEN E MIDPOINT OP AC GIVEN F MIDPOINT OP BD READY M 15 MIDPOINT OP AD TO - BE - PROVED PROOF : TOP DQUN SEUICH: < DPC = < BPK IDENTITY DP = BF BY - MID - POINT CDP = < KBP PARALLEL - OR - ANTIPARALLEL - SIDES THEREFORE: TRIANGLE DPC CONGRUENT TO TRIANGLE BFK AS^ THERBFORE: FC = PK BY - CONGRUENT - TRIANGLES P IS YIDWINT OF CK E0 - SIDES E IS UIDWINT O? CA DATABASE THEREPORE: AK PARALLEL TO EP BY TWO YIDPOINTS IN TRIANGL8 AKC AK II D€ DATA0ASE M II a PROMD mFsFoRE: M // DC BY - TWSITIVITY - OP - PARALLELISY a // DC PROVED E IS MIDPOINT OF AC DATABASE TWBREPORE: W IS THE MIDPOINT OP AD BY BISECTION O? THIRD SIDE IN TRINIGLE *M: THEREFORE: U=W BY - MID - WINT Q.E.D. &le-Sidr-Anpls (angula-lado-anpulol. Se refiere al critsrlo de conpruencia ernpasido por el prowani.. ENSEÍ~NZA DE LAS CIENCIAS, 1988, 6 (1) OTROS TRABAJOS Sin embargo el demostrador de teoremas de Giorgiutti hace ya aparecer, antes de ofrecer la demostración, algún tipo de menú en la pantalla: por ejemplo, jnecesitas ayuda?, ¿no necesitas ayuda? En el primer caso un nuevo menú ofrecena una pista especvica o bien un listado de teoremas utilizados (o simplemente relacionados con el tema) entre los que el sistema ha manejado de su base de datos o ha ido obteniendo y que son pertinentes para la demostración. Pueden ahora aparecer los enunciados de estos teoremas y sus corolarios más importantes; o, en otro caso, ofrecer pistas de diferentes niveles de dificultad, según el lugar del resultado parcial en el árbol de deducciones: jsabes probar que AK es paralelo a EF?, jsabes probar que el tiriángulo DFC es congruente con el triángulo BFK? etc. Evidentemente queda aún un largo trecho que recorrer -en las dos aproximaciones al tema que hemos comentadohasta explotar totalmente las potenciales aplicaciones didácticas de estos avances matemáticos. 2. IMPLICACIONES DIDACTICAS DE LOS PROGRAMAS DE DEMOSTRACION AUTOMATICA Una parte de este trabajo de acomodación de estas herramientas a las situaciones de enseñanza/aprendizaje consiste, en nuestra opinión, precisamente en el análisis general de sus implicaciones didácticas. Análisis que esbozamos en esta parte del artículo considerando tres aspectos: ámbito donde se circunscribirían tales imglicaciones, consecuencias teóricas y observaciones nietodológicas derivadas de las mismas. El primer aspecto hace referencia, naturalmente, al papel de la enseñanza de las técnicas de demostración (o del propio concepto de demostración) en los objetivos de la enseñanza actual de las matemáticas. Podemos constatar el interés, patente en documentos de nuestras autoridades educativas y reflejo de una corriente amplia de opinión entre los profesores, por explicitar como objetivos de esta enseñanza la introducción en el método científico (definir, conjeturar, demostrar) y en el razonamiento lógico (MEC, sin fecha). Por otra parte se hace hincapié, metodológicamente, en el papel de las matemáticas «como útil instrumento para la resolucicin de problemas)) (Arrieta, 1986), en ((resaltar el sentido práctico de las matemáticas)) (MEC, 1984), lo que se traduce -por ejemploen la realización de actividades geométricas entroncadas en la vida cotidiana del alumno. El actual desarrollo de un enfoque heurístico en la enseñanza de las matemáticas puede contemplarse -además de desde otros puntos de vistacomo una adecuada síntesis de los objetivos (razonamiento lbgico-cientifico) y métodos (resolución de problemas interesantes). Como seííaló Polya hace muchos años, sólo las matemáticas proporcionan las mejores oportunidades para que los alumnos no universitarios se enfrenten a auténticos problemas con posibilidad de resolverlos en un nivel auténtico científico. Indudablemente la vigencia de estas tendencias didácticas debe conllevar también una revitalización del uso de demostraciones en geometría elemental -después de todo, las distintas estrategias para resolver un problema geométrico conducirían a una prueba de la solución adoptada. Parece, pues, que es oportuno concluir la actualidad e interés del tema de la enseñanza de la demostración en geometría -y en particular de los aspectos que se refieren al posible uso didáctico de material informático que efectúa tales demostraciones. Sin embargo -y aquí entramos en la segunda parte de nuestro análisisno es precisamente la vía del uso de algoritmos o de mecanismos que los soportan la más próxima a un enfoque heurístico. Sin duda la aproximación que hemos comentado mediante técnicas de Inteligencia Artificial se acerca algo a tal enfoque en el planteamiento de los creadores de los programas, aunque no en el fin para el que éstos se conciben: la demostración automática. Esta reflexión parece invalidar la posibilidad de que estas técnicas informáticas tengan una aplicación en la enseñanza actual. Entendemos que tal invalidación es sólo aparentemente y que existen algunas consecuencias fundamentales que se derivan de la mera existencia y efectividad de estos paquetes de demostración. En primer lugar ello implica una matización radical respecto de la relación -mencionada tanto en los documentos del MEC citados, como en la opinión de Polya recogida arribaentre aprendizaje de las matemáticas e iniciación al método cientifico o al razonamiento lógico. Indudablemente uno y otro se enfrentan en la vida cotidiana o en las ciencias (de cualquier índole), habitualmente, con problemas para los que no se conoce «a pnori)) un mecanismo de resolución. Sin embargo entrenamos a nuestros alumnos, preferentemente, en la resolución de problemas que sí poseen efectivamente (y no sólo teóricamente) tales mecanismos. Aún sin cuestionar lo adecuado de ese campo de entrenamiento, jno sería más honesto advertir -a profesores y alumriosde la radical diferencia epistemológica entre uno y otro tipo de situaciones? Por otra parte, si la aparición de las calculadoras supuso (y aún supone) un debate entre los profesionales de la enseñanza sobre el papel y los límites del aprendizaje de las destrezas del cálculo aritmético, jno debería suscitarse otro debate similar en el futuro sobre la resolución de problemas geométricos? ¿Podrán o no podrán nuestros alumnos resolver las tareas propuestas -como el problema típico de inscribir un cuadrado en un triángulo, manejado por Polyausando un ordenador personal con un paquete de demostración automática? ENSEÑANZA DE LAS CIENCIAS, 1988, 6 (1) OTROS TRABAJOS Naturalmente, en una enseñanza heurística de las matemáticas el conocimiento de la solución a un problema no es precisamente el objetivo final sino el aprendizaje de las técnicas que conducen a su descubrimiento (aunque también antes se decía que el objetivo final de la realización de tediosas operaciones aritméticas no era el resultado sino el ejercicio mental involucrado). Y sin embargo la posibilidad de saber, con una máquina auxiliar, la solución puede eliminar motivación.. . REFERENCIAS BIBLIOGRAFICAS ANDERSON, J.R., BOYLE C.F., YOST G., 1985, The Geometry Tutor, Proceedings IJCAI'85, Los Angeles, pp. 1-7. ARRIETA, J., 1986, La teoría de Piaget y el desarrollo Curricular en Matemáticas. A De las estructuras a las funciones. Actas Simposio Psicología del Aprendizaje y Desarrollo. Oviedo. COELHO, H., MONIZ PEREIRA, L., 1986, Automated Reasoning in Geometry Theorem Proving with Prolog. Journal of Automated Reasoning 2, pp. 229-290. Cabe, en fin, explorar la acomodación metodológica de estos demostradores automáticos, enriqueciendo con ellos las técnicas actuales de enseñanza. Implementar los modos de comunicación en situaciones de aprendizaje es inforrnáticamente sencillo (más que crear los programas de demostración), pero extraordinariamente complejo desde un punto de vista didáctico y exige una investigación que apenas ha comenzado (aunque véase lo que hemos comentado sobre el programa de Giorgiutti). GIORGIUTTI, I., 1986, Comunicación al IREM Universidad de Rennes. HADZIKADIC, M., LICHTENBERGER, F., YUN, D.Y., 1986, An Application of Knowledge - Base Technology in Education: A Geometry Theorem Prover. Actas SYMSAC 86. University of Waterloo. MEC, (sin fecha). Hacia la Reforma. Dirección Gral. de EE.MM. Madrid. MEC, 1984, Anteproyecto para la reforma del Ciclo Superior de la E.G.B. Dirección General de Educación Básica.