The Naproche project (Natural language Proof Checking) studies the semi-formal language of mathematics from a linguistic, philosophical and mathematical perspective. A central goal of Naproche is to develop a controlled natural language (CNL) for mathematical texts and adapted proof checking software which checks texts written in the CNL for syntactical and mathematical correctness.
The Naproche system is an implementation of the ideas developed by the Naproche project. It accepts a controlled but rich subset of ordinary mathematical language including TeX-style typeset formulas and transforms them into formal statements. Linguistic techniques are adapted to allow for common grammatical constructs and to extract mathematically relevant implicit information about hypotheses and conclusions. Finally, automated theorem provers are used to prove the correctness of the input text.
For an overview over the linguistic and logical techniques developed for the Naproche system, see this paper.
A detailed description and analysis of the logical and linguistic techniques developed within the Naproche project can be found in Marcos Cramer's PhD thesis. In Sections 7.2 to 7.4 of the thesis, there is a detailed description of the Naproche CNL. In Appendix D of the thesis there is a concise manual of the Naproche system.
The Naproche activities have developed in two directions pursued by two groups that are in close contact and cooperation.
The Naproche-prover group is the more mathematical group developping a prover for a controlled natural language. Its work is based on SAD as developed by Andrei Paskevich.
The Naproche-FRAME group is oriented towards linguistics and text technology. Currently, it is not developing a complete system, but the mid- to long-term goal is to eventually develop a library of frames and an interface that can be connected to provers, proof checkers and tutorial systems.
The Diproche (DIdactical PROof CHEcking) project pursues the goal of using natural language proof checking for teaching students elementary proving techniques. Currently, the system processes proofs written in a controlled fragment of German and gives feedback on language, type correctness, logical correctness, achievement of proof obligations, use of formally fallacious reasoning and, in some cases, provides counterexamples to false steps. It covers the areas of elementary propositional logic, Boolean set theory, elementary number theory and axiomatic geometry, with further areas in development. For further information see https://arxiv.org/abs/2006.01794v3.