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

翻译：自动推理系统在中学的引入面临若干瓶颈。除了课程设置与教师层面的问题外，几何自动定理证明的输出结果与学校常规的猜想证明教学实践之间的脱节，成为此类工具在教学中广泛推广的主要障碍。自早期几何自动定理证明系统实现以来，基于人工智能方法、采用推理规则的前向链式推理的综合型证明器被认为更适用于教育目的。选择适当的规则集以及能运用这些规则集的自动化方法是一项重大挑战。本文讨论了一种规则集及其基于几何演绎数据库方法(GDDM)的实现。我们选取若干适合七年级学生（约12岁）的几何猜想对该方法进行了测试。文中还提出了一份教案，旨在介绍几何定理证明的形式化演示方法，并以此激发学生的学习动力。