We show here how write a simple arithmetic calculation as a structured derivation and check the correctness of the calculation with the automatic checker. The checker give us objective feedback on whether the derivation is correct, or whether there are errors or problematic steps that need to be fixed. In the latter case, we fix the errors and then check again.
The way a student works with the automatic checker is similar to the test-debug cycle in programming. A programmer writes a program with an editor that understands the syntax of the programming language. The program is then run with test data on a a computer. The first run often results in syntax errors, execution errors, and/or wrong results for the given test data. This is the test phase, where the computer indicates errors in the program. After this comes the debug phase, where the programmer studies the errors, tries to understand why they occur, and then tries to fix the errors. Then back to the test phase again, running the program with same or different test data. The debug phase starts again, if there are still errors. This is repeated as long as there are errors that are detected by the test data.
A student solving a math problem in the eMath Studio environment works in the same way. The student writes the solution of a math problem with the eMath Editor, which understands structured derivations. The student then checks the solution with the eMath Checker. If this shows that each step is correct, then the solution is mathematically correct. If the checker gives error messages or warnings, then the student starts the debugging phase, fixing syntax errors, trying to understand why some steps could not be proved correct, and fixing these steps. Then the cycle is repeated: check the solution with the checker, and fix the remaining errors. The work is done when the checker accepts the solution as correct.
In both cases, the end result is a product that is correct in the appropriate sense: the program gives the right results for the test data, and the students solution is mathematically correct.
We demonstrate how this process works below, with videos and discussions.
Creating a Calculation with the Editor
Our first short video shows how to create a calculation in eMath Studio.
This is the calculation that we created in the video:
The calculation is shown as a structured derivation:
- each formula in a calculation is written on its own line
- the relation between the formulas (here equality) is written on a line between the formulas
- the relation is followed by a justification (in curly brackets) that explains what was done or why the relation holds between the expressions.
This means that each calculation step comes with an explicit justification. This makes it easy to explain the calculation for students, easy for students to understand the calculation later on, and easy for students to understand their own calculations later on. Moreover, this syntax is precise enough so that a computer can understand it and check its correctness.
Checking that the calculation is correct
Next we show how to use eMath Checker to check whether the calculation is correct. The checker goes through the calculation step-by-step, and tries to prove that each step is correct.
The calculation is mathematically correct, if each step is proved correct.
Note that there is no underlying model solution that the checker uses, the checker will accept any calculation that is mathematically correct.
Fixing Calculation Errors
The last video shows how to fix the errors that the checker finds in the solution.
The big advantage here is that the student gets immediate feedback on his/her own solution, while working on the solution. The checker gives positive reinforcement by showing which steps are correct, and directs the student’s attention to the steps that are wrong or problematic. The student learns how to solve this kind of problems by fixing the errors.
The checker will either mark a step as correct (check mark), or give a syntax error (X-mark), or a warning (exclamation mark). A syntax error means that the checker has not understood some part of the derivation, usually because a formula is written in the wrong way. A checker warning means that the checker was not able to prove a calculation step correct. The three main reasons are:
- the step is not correct mathematically ,
- the proof was too difficult, or
- there is missing information.
The first reason is by far the most common. A calculation step that is wrong cannot be proved correct. The second reason means that the checker has run out of time, it has exceeded its given time quota. The last reason means that the checker is asked to prove a step that requires information that it does not have. This could be some assumptions that have not been given to it, or some mathematical notation that it does not know about, or some mathematical properties or theorems that it does not know.
