Automated Theorem Proving in the Classroom

Wolfgang Windsteiger
(Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz (JKU), Altenbergerstr. 69, 4040 Linz, Austria)

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.

Invited Lecture in Predrag Janičić and Zoltán Kovács: Proceedings of the 13th International Conference on Automated Deduction in Geometry (ADG 2021), Hagenberg, Austria/virtual, September 15-17, 2021, Electronic Proceedings in Theoretical Computer Science 352, pp. 54–63.
Published: 30th December 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: