# The Original Naproche
Projekt (2003–2015)

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.

# Current groups

The Naproche activities have developed in two directions pursued by
two groups that are in close contact and cooperation.

## The Naproche-prover group
(since 2015)

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
(since 2015)

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.