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岁的学生)的目标。提出一个课程计划的目的是正式证明几何理论,试图激励学生实现这一目标。</s>