author = {W. Windsteiger},
title = {{Theorema 2.0: Automated and Interactive Theorem Proving in Math Education}},
language = {english},
abstract = {The Theorema system is a mathematical assistant system that is designed to support a mathematician during all phases of mathematical activity. The focus lies, however, on proving mathematical theorems. Theorema employs algorithms that aim at generating proofs in a "natural style" that can then also be presented in a style similar to how proofs are given in textbooks. In the context of teaching the method of proving (for math/CS students at undergraduate university level) the system can be used in fully automated mode or interactive mode. In fully automated mode students state the proposition to be proven, compose the knowledge base, then just hit the "Prove"-button, and finally get the successful proof, which they can study as if it was given to them by the teacher. In case of a failing proof, the proof can still be displayed and the reason for failure can be investigated (which is in many cases a very valuable exercise for students!). In interactive mode, students can interfere the automated proof generation in various ways, e.g. the choice of the next inference rule to apply, choice of the branch in which to proceed with the proof, choice of variable instantiation, etc. While in the learning phase, the interactive mode is very useful because it proposes the student only inference rules that are actually applicable in the current state, and it eliminates errors in the execution of a rule, e.g. when performing a wrong rewrite or instantiation step. With this talk, we want to initiate discussions on how to teach the method of proving to students at different levels. In particular, we are interested in opinions whether computer-support in this kind of teaching is desirable and, if yes, what are the requirements for computer systems to be used in the classroom.},
year = {2013},
month = {June 10},
note = {Contributed talk at CSASC'2013, Koper, Slovenia},
conferencename = {CSASC'2013, Koper, Slovenia}