通过自动化证明生成改进 QED-Tutrix

以技术工具辅助教师的想法并不新鲜。数学一般而言，几何尤其，在开发教育软件时提出有趣的挑战，无论在教育还是计算机科学方面。QED-Tutrix 是一个几何智能导师，提供界面以帮助高中生解决证明问题。它聚焦于特定目标：1) 允许学生自由探索问题及其图形，2) 以任意顺序接受证明元素，3) 处理可由教师定制的多种证明，4) 能够在问题求解的任何步骤帮助学生（若有需要）。该软件也独立于教师的干预。QED-Tutrix 提供了一条几何教育的有趣途径，但目前受限于实现新问题的过程冗长，该任务仍须手动完成。因此，QED-Tutrix 研究团队的主要焦点之一是通过自动化寻找给定问题所有可能证明这一繁琐步骤来简化新问题的实现。该自动化须遵循基本约束以创建与 QED-Tutrix 兼容的问题：1) 证明的可读性，2) 高中水平的可及性，3) 教师修改定义证明“可接受性”参数的可能性。我们在本文中呈现对此任务可能途径的初步探索结果。几何自动定理证明是研究广泛的课题，存在多种证明器。然而，我们的约束相当特定，使用现有证明器需做些适配。因此我们实现了一个自动化证明器原型以满足需求。未来目标是在我们的特定用例中比较现有证明器与我们的实现之间的性能与可用性。