Deep understanding and skilled usage of mathematics and logic are essential ingredients of most scientific and engineering activities, particularly in the fields of Mathematics and Computer Science, but also in many other areas. In Information Technology applications, these skills are becoming crucial as the systems become more and more complex and only the use of formal techniques can guarantee their proper behaviour.
Unfortunately - as the first author has learned over many years of didactic and research activity in mathematical logic - practical training in this field is severely under-emphasized in the vast majority of Math and Computer Science curriculla all over the world. In contrast, at RISC-Linz we have offered for over a decade a comprehensive study and training program in mathematical logic and practical problem solving and proving [Buchb-Licht:81]. Based on this experience we are now in the position to develop concrete tools for the practical usage of the working mathematicians and for the students, which can assist them in teaching / learning mathematical logic and proving skills, as well as in mathematical textbook writing, problem solving, and scientific research.
In this paper we present the tools developed in the frame of the Theorema project for the training of students in Computer Science, Mathematics, and Engineering in the language of predicate logic and in establishing proofs in this language. These tools form an interactive theorem prover in high-order logic, written in the computer algebra system Mathematica 3.0 [Wolfram:96], which is presented to the user in the form of an intelligent environment for developing mathematical texts in natural language (e. g. in the style used by scientists in typical text-books).
The main objectives of the formal training in our system are:
- Language training: learn and train the use of mathematical language for concise and exact expressing of models.
- Formal models: learn and train how to build mathematical models for concrete real problems (defining concepts, defining properties, defining and exploring problems).
- Conjecture and prove: learn and train the formulation of conjectures about the properties of mathematical objects, prove and disprove conjectures.
The last activity - proving - is one of the most difficult formal activities for the human intellect, and consequently it requires most of the learning and training. Our system offers computing support for all the objectives mentioned above, however we will emphasize in this paper the proving and the proving-assisting capabilities of our software, which took most of the effort to develop.
We believe that providing computer support to the working scientist and to the engineering student opens the way for:
- a new understading of mathematics and computer science;
- a new level of creativity and productivity in mathematics;
- a new quality of education of teachers and students, both at academic and pre-academic levels.
These aspects are certain to have a "boule-de-neige" effect on the general education in mathematics, computer science, and engineering, with obvious benefic effects on all sectors of human activity.
It is beyond the scope of this paper to document extensively the state-of-the-art in this field, rather we will shortly review this (for more details see [Homann:96], [Buchb-et-al:97]). Currently the most successful and effective computer-assistants for the working scientist are the computer algebra systems, which contain a large collection of mathematical knowledge implemented as mathematical models and algorithms (Mathematica, Maple, Macsyma, Scratchpad, etc.). All these systems have quite efficient computing and solving capabilities (over numerical domains), but none of them offers support for constructing mathematical models and for proving (which is a lot more than just being able to compute with logic formulae - facilites recently added to few such systems).
On the other hand, a long-time research in automated reasoning produced a mature theory and many quite powerful systems for proving, however they are rarely used outside academic laboratories and quite unsuitable for use by non-experts. Their user-interface is most of the time quite cryptic, also the presentation of proofs and the way reasoning is performed differ significantly from the way human mathematicians operate on mathematical models.