  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.
