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

Abstract

El papel relevante de las tareas de validación en la enseñanza tradicional de la geometría se aborda actualmente como una mera introducción al razonamiento lógico. La existencia de algoritmos de prueba automáticos para cualquier teorema de geometría elemental y su reciente implementación en computadoras da un carácter peculiar al tipo de razonamiento utilizado en esta teoría -uno de los pocos es decidible- y modifica su significado educativo. Por otro lado, el análisis de la forma de enseñar geometría muestra un énfasis excesivo en el entrenamiento al descubrir modelos, descuidando el edificio de cuerpos teóricos de conocimiento. Ambos hechos exigen una exploración de nuevas técnicas en la enseñanza de pruebas geométricas; se describen y analiza el uso de software educativo (basado en técnicas de I. A.) para programas a prueba que ahora están funcionando.