Automated Theorem Proving in the Classroom

TL;DR

This paper explores the integration of automated theorem proving software, specifically Theorema, into university logic courses to enhance student motivation and understanding of logic principles, acting as a supportive logic-tutor.

Contribution

It demonstrates how theorem proving software can be effectively used as an educational tool to motivate students and deepen their understanding of logic, rather than just teaching software usage.

Findings

Increased student engagement with logic concepts.

Improved understanding of logic principles.

Software acts as an effective logic-tutor.

Abstract

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.