author = {W. Windsteiger},
title = {{Towards Computer-Supported Proving in Maths Education}},
language = {english},
abstract = {In this work we want to present an environment for learning and teaching mathematics that integrates computer-support for different aspects during different stages of the mathematical learning process. In the first phase of confrontation with new content the student can benefit from computer-powered interactive experiments that help to develop and sharpen the intuition about the concepts involved. Experiments are designed carefully such that they lead the user to the discovery of mathematically interesting properties of the investigated objects. During the strengthening phase, the student is asked to first formulate the observed properties in an exact mathematical language and then prove these propositions. At this point, an automated theorem proving system is employed to assist the student in this task. Interactive elements are based on the symbolic and graphical computation capabilities of the well-known computer algebra system Mathematica, and we use its possibility to connect to Java in order to provide intuitive graphical user interfaces. Algorithms provided by or implemented in Mathematica are employed in these experiments so that a student can not only work with (a few) pre-computed examples but also with user data or randomly generated input. The formal parts are supported by Theorema, a mathematical assistant system also based on Mathematica. Theorema supplies an intuitive two-dimensional input syntax close to common mathematical style and it provides fully-automated or interactive theorem provers for different domains, which generate mathematical proofs in human-readable format. We illustrate the flavor of human-computer-interaction possible in such an environment in examples taken from the learning units on ``Equivalence relations and set partitions'' and ``Polynomial interpolation'' and claim that the computer in classroom can not only be employed for numerical or symbolic computation or visualization but it can contribute also to the realm of teaching mathematical proofs.},
year = {2007},
month = {June 21},
note = {Contributed talk at First Central- and Eastern European Conference on Computer Algebra- and Dynamic Geometry Systems in Mathematics Education (CADGME)},
institution = {University of Pecs},
conferencename = {First Central- and Eastern European Conference on Computer Algebra- and Dynamic Geometry Systems in Mathematics Education (CADGME)},
url = {http://matserv.pmmf.hu/cadgme/}