9-13 June 2013
Koper, Slovenia
UTC timezone
Theorema 2.0: Automated and Interactive Theorem Proving in Math Education
Presented by Wolfgang WINDSTEIGER
Type: Oral presentation
Track: Proving in Mathematics Education at University and at School
Content
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
undergradutate 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.
Place
Location: Koper, Slovenia