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 a quick overview of the Naproche project take a look at this paper. You can try out the latest stable version of Naproche here .


Last changed: 27 Aug 2010. This site is optimized for Opera. Most features also work well in Firefox and Safari.