author = {W. Windsteiger},
title = {{Automated Theorem Proving in the Classroom}},
language = {english},
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 emph{not} to teach students the proper use of a particular piece of software. In contrast, we try to emph{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.},
number = {21-15},
year = {2021},
month = {August},
note = {Extended version of keynote talk at ADG 2021 conference},
keywords = {Theorema, Logic Education},
length = {18},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}