Automated Theorem Proving in the Classroom

Wolfgang Windsteiger

doi:10.4204/EPTCS.352.6

Automated Theorem Proving in the Classroom

Wolfgang Windsteiger

Research Institute for Symbolic Computation

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

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. (Note to publication: Extended abstract)

Original language	English
Title of host publication	Proceedings Automated Deduction in Geometry (ADG 2021)
Editors	Predrag Janicic
Pages	54-63
Number of pages	10
Volume	352
DOIs	https://doi.org/10.4204/EPTCS.352.6
Publication status	Published - 2021

Publication series

Name	Electronic Proceedings in Theoretical Computer Science (EPTCS)
ISSN (Print)	2075-2180

Fields of science

101 Mathematics
101001 Algebra
101005 Computer algebra
101009 Geometry
101012 Combinatorics
101013 Mathematical logic
101020 Technical mathematics

JKU Focus areas

Digital Transformation

Access to Document

10.4204/EPTCS.352.6

Cite this

@inproceedings{3891f58019cd42d88d66b3e34a4c550f,

title = "Automated Theorem Proving in the Classroom",

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. (Note to publication: Extended abstract)",

author = "Wolfgang Windsteiger",

year = "2021",

doi = "10.4204/EPTCS.352.6",

language = "English",

volume = "352",

series = "Electronic Proceedings in Theoretical Computer Science (EPTCS)",

pages = "54--63",

editor = "\{Predrag Janicic\}",

booktitle = "Proceedings Automated Deduction in Geometry (ADG 2021)",

}

TY - GEN

T1 - Automated Theorem Proving in the Classroom

AU - Windsteiger, Wolfgang

PY - 2021

Y1 - 2021

N2 - 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. (Note to publication: Extended abstract)

AB - 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. (Note to publication: Extended abstract)

U2 - 10.4204/EPTCS.352.6

DO - 10.4204/EPTCS.352.6

M3 - Conference proceedings

VL - 352

T3 - Electronic Proceedings in Theoretical Computer Science (EPTCS)

SP - 54

EP - 63

BT - Proceedings Automated Deduction in Geometry (ADG 2021)

A2 - Predrag Janicic, null

ER -