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 .

News

• 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 diplom 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.