Learning to Reason Assisted by Automated Reasoning

We report on using logic software in a novel course-format for an undergraduate logic course for students in computer science or artificial intelligence. Although being designed as the students' basic introduction to the field of logic, the course features a novel structure and it adds some modern content, such as SAT and SMT solving, to the traditional and established topics, such as propositional logic and first order predicate logic. The novel course design is characterized by, among others, the integration of existing logic software into the teaching of logic. In this paper we focus on the module on first-order predicate logic and the use of the Theorema system as a proof-tutor for the students. We report on statistical evaluation of data collected over two consecutive years of teaching this course. On the one hand, we asked for feedback of students on how helpful they felt the software support was. On the other hand, we evaluated their results in the exams during the course and their development over the entire teaching period. The performance in exams is then correlated with students' own perception of the helpfulness of software.