论文标题
在中学引入自动扣除的四个几何问题
Four Geometry Problems to Introduce Automated Deduction in Secondary Schools
论文作者
论文摘要
中学自动扣除系统的引入面临几个瓶颈，课程中缺乏严格的数学演示主题，教师缺乏有关该学科的知识以及通过自动手段解决任务的困难。 尽管存在这些困难，但我们声称可以通过解决特定情况来引入几何学的自动扣除主题：由学生和老师操纵易于操作，并且可以通过自动扣除工具来处理相当容易的处理。 通过解决四所中学几何问题来讨论该主题：它们的严格证明，视觉证明，数字证明，代数形式证明，合成的正式证明或缺乏它们。对于这些问题，我们讨论了一项课程计划，借助信息和通信技术，更具体地说，是自动扣除工具。
The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject of rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers about the subject and the difficulty of tackling the task by automatic means. Despite those difficulties we claim that the subject of automated deduction in geometry can be introduced, by addressing it in particular cases: simple to manipulate by students and teachers and reasonably easy to be dealt by automatic deduction tools. The subject is discussed by addressing four secondary schools geometry problems: their rigorous proofs, visual proofs, numeric proofs, algebraic formal proofs, synthetic formal proofs, or the lack of them. For these problems we discuss a lesson plan to address them with the help of Information and Communications Technology, more specifically, automated deduction tools.
