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

Resumen

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ática para cualquier teorema de geometría elemental y su implementación reciente en las computadoras le da un carácter peculiar al tipo de razonamiento utilizado en esta teoría, uno de los pocos que son decidibles, y modifica su significado educativo. Por otro lado, el análisis de la forma de enseñar geometría muestra un énfasis excesivo en la capacitación al descubrir modelos, descuidando la construcción de cuerpos teóricos de conocimiento. Ambos hechos exigen una exploración de nuevas técnicas en la enseñanza de pruebas geométricas; Describimos y analizamos el uso de software educativo (basado en técnicas de IA) para los programas de prueba automáticos que ahora funcionan.