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.

News

• 28.07.2014 Web Interface deactivated, as Naproche 0.5x does not run on the web interface, but needs to be installed.
• 26.01.2013 Naproche 0.52 released
Some bugs of Naproche 0.51 have been removed.
• 32 bit: naproche052-i686.tgz
• 64 bit: naproche052-x86_64.tgz
• 21.03.2012 Naproche 0.51 released
Naproche 0.51 is significantly faster than Naproche 0.5 and has some bugs removed (especially the bug that previously made the 64 bit release unusable).
• 32 bit: naproche051-i686.tgz
• 64 bit: naproche051-x86_64.tgz
• 19.01.2012 Naproche 0.5 released
Naproche 0.5 is no longer available through a web interface, but has to be installed. We only provide distributions for Linux:
• 32 bit: naproche-i686.tgz
• 64 bit: naproche-x86_64.tgz (not functioning; use Naproche 0.51)
• 18.08.2010 Papers and Releases
• Dörthe Arndt's diploma thesis added to downloads.
• The premise selection algorithm is available as a stand alone program at http://code.google.com/p/tptpaxsel/
• Work on Naproche 0.5 has started. The web interface version will still be supported, but not developed further.
• 08.06.2010 Naproche 0.47 released
• Prepositions support added.
• IJCAR Paper added to downloads.
The detailed list of changes can be found here.
• 25.03.2010 Naproche 0.46 released
• Several Minor Bugfixes.
• We are currently working on a Naproche version of Euclid's Elements.
The detailed list of changes can be found here.
• 7.12.2009 Naproche 0.45 released
• 'the' sentences are now supported. e.g. "The set of natural numbers is infinite."
• Improved output.
The detailed list of changes can be found here.
• 1.11.2009 Naproche 0.41 released
Version 0.41 of Naproche is now online. The list of changes can be found here.
• 1.10.2009 Naproche 0.4 released
Version 0.4 of Naproche is now online. The list of changes can be found here.