The introduction of automated deduction systems in secondary schools face
several bottlenecks. Beyond the problems related with the curricula and the
teachers, the dissonance between the outcomes of the geometry automated theorem
provers and the normal practice of conjecturing and proving in schools is a
major barrier to a wider use of such tools in an educational environment. Since
the early implementations of geometry automated theorem provers, applications
of artificial intelligence methods, synthetic provers based on inference rules
and using forward chaining reasoning are considered to be more suited for
education proposes. Choosing an appropriate set of rules and an automated
method that can use those rules is a major challenge. We discuss one such rule
set and its implementation using the geometry deductive databases method
(GDDM). The approach is tested using some chosen geometric conjectures that
could be the goal of a 7th year class (approx. 12-year-old students). A lesson
plan is presented, its goal is the introduction of formal demonstration of
proving geometric theorems, trying to motivate students to that goal

介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。