四道几何题引入中学自动演绎
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
