The proof checker

With the development of a proof checker for the $\mmath$-language, we are approaching two objectives: On the one hand it should confirm that the semantics of the $\mmath$-language is stated unambigously and precisely enough to be implemented in a computer program. On the other hand it should provide a tool for students to train compliance with the formal mathematical rules. Traditionally, students hand in their exercise on paper and get written feedback from their tutor a week later. In contrast to this approach such a tool has the big advantage of providing immediate feedback.

A first step in the development of the proof checker is the design of a surface syntax. It should be easy enough to be parsed by a computer, but also comprehensible for the average student. For this purpose it provides classical concepts like infix notations, for example.

In order to reflect the imperative character of the $\mmath$-actions, the proof checker is implemented as a state-based program. Starting from an initial state, consisting of some names and valid propositions crucial for the working of the system, it takes the written actions and checks their correctness by checking their requirements on that state and altering it based on the rules described by the semantics of the language.

The $\mmath$ proof checker is not designed as an automatic proof system or an interactive proof assistant. However, it integrates aspects of both of them in its system. One can observe that mathematicians tend to omit certain arguments in their proofs -- namely those who may seem obvious for the target group. In early calculus courses, for example, the distributive or the commutative law for real numbers are likely to be omitted. Since the system aims to support the average mathematician, the proof checker provides mechanisms called strategies for this proof omitting as well. Strategies are rules being invoked whenever the checker detects that an action cannot be performed because some required valid statements are missing. Then, the strategies try to fill the gap by finding the validity of these statements as well, for example, by using internal rules of the languages or by applying valid theorems.

A proof assistant functionality arises by the rule checking process itself. Since the requirements for every action are stated precisely, the checker can tell exactly which requirements are missing to complete the action and give an appropriate error message to the user. The user then can add the proof for the missing requirement to his text and restart the checking process.