基于规则的定理证明器：中学证明入门

在中学引入自动演绎系统面临若干瓶颈。除了与课程和教师相关的问题外，几何自动定理证明器的输出与学校中猜想和证明的常规实践之间的不协调，是此类工具在教育环境中更广泛应用的主要障碍。自几何自动定理证明器的早期实现以来，基于推理规则并使用前向链推理的综合证明器被认为更适合教育用途。选择合适的规则集以及能够使用这些规则的自动方法是一项重大挑战。我们讨论这样一组规则及其使用几何演绎数据库方法（GDDM）的实现。该方法使用一些选定的几何猜想进行了测试，这些猜想可以作为七年级（约12岁学生）班级的目标。我们提出了一份教案，其目标是引入形式化演示来证明几何定理，试图激励学生达到该目标。