Title: From Computing to Proving: Experiments with THEOREMA in Mathematics Education

Author: Franz Lichtenberger* (franz.lichtenberger@scch.at)

Affiliation: Research Institute for Symbolic Computation, Hagenberg, Austria

Abstract: 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 course is "The Language and Methods of Mathematics" and it is radically different from traditional, calculus-based math courses for freshmen. We will give several examples where students have to give formal definitions of notions in areas relevant to programming like sequences, trees, graphs etc. and then have to prove properties of and relations between objects of those 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.