From computing to proving: Experiments with theorema in math education

Autoren Franz Lichtenberger
TitelFrom computing to proving: Experiments with theorema in math education
NoteAbstract at 2001 Conf. on Applications of Computer Algebra (ACA'01). Albuquerque, NM, USA, May/June 2001

THEOREMA is a language and system which aims at combining general predicate logic proof methods and special proof methods for special areas of mathematics in one coherent system. It was developed by Bruno Buchberger and his team at RISC-Linz and is implemented in MATHEMATICA. We use THEOREMA in lab exercises for the mathematics course for first year students of software engineering. The subtitle of the courese is "The Language and Methods of Mathematics" and it is radically different from traditional, calculus-based math courses for freshmen. We will give severalexamples where students have to give formal definitions of notions in areasrelevant to programming like sequences, trees, graphs etc. and then have toprove properties of and relations between objects of that types. We will analyse the benefits of that approach, but also report of difficulties students have with using the system in its current state and with doing this kind of mathematics per se.