Naproche - Natural Language Proof Checking
"; ?>

About Naproche

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.


Last changed: 14 June 2018.