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

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 decidible— and 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.