论文标题
自动化的定理在课堂上证明
Automated Theorem Proving in the Classroom
论文作者
论文摘要
我们报告了在大学教育中使用自动定理证明软件的几种情况。特别是，我们专注于在计算机科学或人工智能中为学生提供软件增强逻辑课程中的理论系统。在我们的教学中使用逻辑软件的目的不是教学生正确使用特定软件。相比之下，我们试图使用某些软件来激发学生的动力，并支持他们通过课程后应该理解的逻辑原则的理解。从某种意义上说，我们试图让该软件充当逻辑指导，该软件不是我们教授的其他主题。
We report on several scenarios of using automated theorem proving software in university education. In particular, we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is not to teach students the proper use of a particular piece of software. In contrast, we try to employ certain software in order to spark students' motivation and to support their understanding of logic principles they are supposed to understand after having passed the course. In a sense, we try to let the software act as a logic-tutor, the software is not an additional subject we teach.
