One major use of the Theorema software is for training students how to construct mathematical proofs. The provers can be used at various level of interaction:
The student studies the proofs produced automatically (eventually embeded in a textbook), in one of the follwing formats:
- printed on paper (when no computer is available),
- as HTML files (when no Mathematica software is installed),
- as Mathematica notebooks (needs only the free version of the Mathematica software).
The later two versions have the advantage that the proofs can be read at various levels of details, and they are also accessible over the internet.
The passive mode is intented to be used in the early stages of the proof-training process, when the teacher introduces the students to the proof-techniques in classroom presentations, and the students study individually the lecture notes distributed either on paper or electronically.
The student uses the Mathematica software and the Theorema software in order to produce proofs for a collection of theorems distributed by the teacher.
This mode is suitable for the more advanced students, who can now interact with the system by modifying the theorems, adding new assumptions, proving additional lemmas, etc. In this way they get more insight into the proving mechanisms and they begin to train in formal model construction.
It is important to note that this increased level of interaction allows the students to learn individually at their own pace. This is crucial aspect in proof training, because typically the students have different background in formal mathematics, and also in various mathematical fields: some proof techniques are more familiar to ones than to the others because they are more used in the field of their particular background.
In addition to the Theorema provers, the student uses a special set of functions allowing a more intimate interaction with the provers. Namely, the proof is displayed in a step-by-step fashion, and the user has the possibility to direct the process in various ways:
- navigate back and forward through the proof;
- remove redundant assumptions in order to simplify the proof;
- introduce additional subgoals in order to speed-up the process or to give "hints" when the problem is to complicated to be solved automatically;
- indicate which proof technique should be used at which point in the proof, etc.
Figure 1 presents a typical screen when using the predicate-logic prover in active mode, with several Mathematica notebooks:
- "Proof Control" displays various buttons for controlling the proofs and the level of interaction.
- "Textbook" contains the theorems to prove. By selecting a command of type
"Proof[...]" and then pressing "Execute" from the proof control window, the proof is initiated.
- "Proof Window" contains the actual text of the proof. In interactive mode, the partial proof obtained at the current stage is displayed with grey cells for the still unsolved subproofs and with framed cells for the most recent proof step which was executed. By pressing "Next Step" in proof control a further proof step will be executed.
- "Proof Situation" shows the current goal (formula to be proven) and assumptions.
- "Log Window" shows a trace of the proof steps and other operations performed.
The software has been already used in the classroom in the frame of the RISC lecture "Thinking, Speaking, Writing" on mathematical logic and proof training.
For instance, a group of 7 students - already medium advanced - have been given a set of 25 proving problems as an interactive textbook, which they examined using the theorema software for 60 min. in interactive mode. By short tests before and after the session we detected that all the students improved their proving skills.
During next November we will perform more classroom tests on a group of new PhD students at RISC, in all the interactive modes. The results will be shortly summarized in the final version of this paper.
