=Paper=
{{Paper
|id=Vol-448/paper-9
|storemode=property
|title=The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts
|pdfUrl=https://ceur-ws.org/Vol-448/paper10.pdf
|volume=Vol-448
|dblpUrl=https://dblp.org/rec/conf/cnl/CramerKKSV09
}}
==The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts==
https://ceur-ws.org/Vol-448/paper10.pdf
The Naproche Project
Controlled Natural Language Proof Checking
of Mathematical Texts
M. Cramer, P. Koepke, D. Kühlwein, B. Schröder, and J. Veldman
University of Bonn and University of Duisburg-Essen
{cramer,koepke,kuehlwei,veldman}@math.uni-bonn.de,
bernhard.schroeder@uni-due.de
http://www.naproche.net
1 Outline of the Naproche Project
The Naproche project1 (NAtural language PROof CHEcking) studies the semi-
formal language of mathematics (SFLM) as used in journals and textbooks from
the perspectives of linguistics, logic and mathematics. A central goal of Naproche
is to develop and implement a controlled natural language (CNL) for mathe-
matical texts which can be transformed automatically into equivalent first order
formulas by methods of computational linguistics. Since parts of mathematical
texts are strictly formal, we expect that a mathematical CNL can cover many
aspects of SFLM.
Further work in the project is directed towards automatic manipulation and
proof checking of CNL texts and the translation of extensive mathematical the-
ories into the Naproche CNL.
2 The Semi-Formal Language of Mathematics
As an example of the semi-formal
√ language of mathematics (SFLM), we cite a
proof for the theorem “ 2 is irrational ” from Hardy-Wright’s introduction
to number theory [2].
√
If 2 is rational, then the equation a2 = 2b2 is soluble in integers a, b
with (a, b) = 1. Hence a2 is even, and therefore a is even. If a = 2c, then
4c2 = 2b2 , 2c2 = b2 , and b is also even, contrary to the hypothesis that
(a, b) = 1.
SFLM incorporates the syntax and semantics of the general natural language,
so that it takes over its complexity and some of its ambiguities. However, SFLM
texts are distinguished from common language texts by several characteristics:
1
Naproche is a joint initiative of Peter Koepke (Mathematics, University of Bonn)
and Bernhard Schröder (Linguistics, University of Duisburg-Essen).
– They combine natural language expressions with mathematical symbols and
formulas, which can syntactically function like noun phrases or sub-proposi-
tions.
– Constructions which are hard to disambiguate are generally avoided.
– Mathematical symbols can be used for disambiguation, e.g. by use of vari-
ables instead of anaphoric pronouns.
– Assumptions can be introduced and retracted. For example, the proof cited √
above is a proof by contradiction: At the beginning, it is assumed that 2
is rational. The claims that follow are understood to be relativised to this
assumption. Finally
√ the assumption leads to a contradiction, and is retracted
to conclude that 2 is irrational.
– Mathematical texts are highly structured. At a global level, they are com-
monly divided into building blocks like definitions, lemmas, theorems and
proofs. Inside a proof, assumptions can be nested into other assumptions, so
that the scopes of assumptions define a hierarchical proof structure.
– Definitions add new symbols and expressions to the vocabulary and fix their
meaning.
– Proof steps are commonly justified by referring to results in other texts, or
previous passages in the same text. So there are intertextual and intratextual
references.
3 The Naproche CNL
The Naproche CNL is currently a small subset of SFLM which includes some of
the above mentioned characteristics of SFLM.
A Naproche text is structured by structure markers: Theorem, Lemma, Proof
and Qed. A theorem is presented after the structure marker Theorem, and its
proof follows between the structure markers Proof and Qed.
First order formulas can be combined with natural language expressions to
form statements, definitions and assumptions.
Assumptions are always opened by an assumption trigger (e.g. let, consider,
assume that . . . ), and closed by a sentence starting with thus or by a Qed.
Definitions always start with define. Assertions are made by statements starting
with a statement trigger (then, hence, therefore, so, . . . ) followed by a first order
formula or a naturally predicated term. Additionally, negation, quantification
and implication may be expressed in natural language.
The proof cited above can be reformulated in the Naproche CNL as follows:
√
Theorem. 2 is irrational.
Proof. √
Assume that 2 is rational. Then there are integers a, b such that a2 =
2b2 and (a, b) = 1. Hence a2 is even. Therefore a is even. So there is an
integer c such that a = 2c. Then 4c2 = 2b2 and 2c2 = b2 . So b is even.
Contradiction. Qed.
This is the actual graphical appearance of the text, since Naproche uses the
mathematical WYSIWYG editor TeXmacs.
4 Proof Representation Structures
Texts written in the Naproche CNL are translated into Proof Representation
Structures or PRSs (see [4], [6]). PRSs are Discourse Representation Structures
(DRSs, [3]), which are enriched in such a way as to represent the distinguishing
characteristics of SFLM discussed in section 2.
A PRS has five constituents: An identification
number, a list of discourse referents, a list of math-
ematical referents, a list of textual referents and an
ordered list of conditions. Similar to DRSs, we can
display PRSs as “boxes” (Figure 1).
Mathematical referents are the terms and formu-
las which appear in the text. As in DRSs, discourse
referents are used to identify objects in the domain
of the discourse. However, the domain contains two
kinds of objects: mathematical objects like numbers
or sets, and the symbols and formulas which are
used to refer to or make claims about mathematical Fig. 1. A PRS with
objects. Discourse referents can identify objects of identification number
either kind. i, discourse referents
PRSs have identification numbers, so that they d , ..., d , mathematical
1 n
can be referred to at some later point. The textual referents m , ..m , condi-
1 k
referents indicate the intratextual and intertextual tions c , ..., c and textual
1 l
references. referents r1 , ..rp
Just as in the case of DRSs, PRSs and PRS con-
ditions have to be defined recursively: Let A, B be
PRSs, X, X1 , . . . , Xn discourse referents and Y a
mathematical referent. Then
– for any n-ary predicate p (e.g. expressed by adjectives and noun phrases in
predicative use and verbs in SFLM), p(X1 , . . . , Xn ) is a condition.
– holds(X) is a condition representing the claim that the formula referenced
by X is true.
– math id(X, Y ) is a condition which binds a discourse referent to a mathe-
matical referent (a formula or a term).
– A is a condition.
– ¬A is a condition, representing a negation.
– A := B is a condition, representing a definition.
– A ⇒ B is a condition, representing an assumption (A) and the set of claims
made inside the scope of this assumption (B).
– contradiction is a condition, representing a contradiction.
Note that contrary to the case of DRSs, a bare PRS can be a direct condition
of a PRS. This allows to represent in a PRS the structure of a text divided into
building blocks (definitions, lemmas, theorems, proofs) by structure markers.
The hierarchical structure of assumptions is represented by nesting conditions
of the form A ⇒ B: A contains an assumption, and B contains the representation
of all claims made inside the scope of that assumption.
The algorithm creating PRSs from CNL
proceeds sequentially: It starts with the
empty PRS. Each sentence or structure
marker in the discourse updates the PRS ac-
cording to an algorithm similar to a standard
DRS construction algorithm but taking the
nesting of assumptions into account. [4]
The PRS constructed from the example
proof is shown on the right (abbreviated and
without the empty reference slots).
5 Translating PRSs into First
Order Logic
PRSs, like DRSs, have a canonical translation
into first order logic and can be processed fur-
ther by logical tools. This translation is per-
formed in a way similar to the DRS to first-
order translation described in [1]. For exam-
ple, the discourse referents normally trigger
existential quantifiers, but in a PRS condi-
tion of the form A ⇒ B the discourse refer-
ents of A trigger universal quantifiers. There
are two main differences between PRS to first-oder translation and DRS to first-
order translation that need discussion:
– The math id-conditions are not translated into subformulas of the first-order
translation. A math id-condition which binds a discourse referent to a term
triggers a substitution of that discourse referent by that term in the transla-
tion of subsequent conditions. A math id-condition which binds a discourse
referent to a formula causes a subsequent holds-condition with that discourse
referent to be translated by that formula.
– Definition conditions are also not translated into subformulas of the trans-
lation. Instead, a condition of the form A := B triggers a substitution of the
relation symbol it defines by the first-order translation of B in subsequent
conditions.
6 Results
We created a program, the Naproche system, which can parse an earlier version of
the Naproche CNL, create the appropriate PRSs, and check them for correctness
using automated theorem provers. The Burali-Forti paradox, a well known
mathematical theorem, as well as several basic statements in group theory, were
formulated in the Naproche CNL, and checked for correctness using the Naproche
system.
7 Related and Future Work
Claus Zinn wrote his PhD thesis about informal mathematical discourse [8].
He used an extended version of DRSs, which he also called Proof Representation
Structures, to represent the meaning of a text. The PRS definitions of Naproche
and Zinn are different.
We are collaborating with the VeriMathDoc project [7], which is developing
a mathematical assistant system that naturally supports mathematicians in the
development, authoring and publication of mathematical work.
We shall extend the Naproche controlled natural language to include a rich
mathematical formula language and many argumentative mathematical phrases
and constructs. Once the Naproche CNL is sufficiently extensive and powerful,
we shall reformulate and check proofs from various areas of mathematics in a
way “understandable” to men and machines.
References
1. Blackburn, P., Bos, J.: Representation and Inference for Natural Language Volume
II: Working with Discourse Representation Structures (1999)
2. Hardy, G. H., Wright, E. M.: An Introduction to the Theory of Numbers (Fourth
Edition, 1960)
3. Kamp, H., Reyle, U.: From Discourse to Logic: Introduction to Model-theoretic
Semantics of Natural Language, Kluwer Academic Publisher (1993)
4. Kolev, N.: Generating Proof Representation Structures for the Project Naproche,
Magister thesis (University of Bonn, 2008), http://naproche.net/downloads.
shtml
5. Kühlwein, D.: A short introduction to Naproche v0.1, http://naproche.net/
downloads.shtml
6. Kühlwein, D.: A calculus for Proof Representation Structures, Diploma thesis (Uni-
versity of Bonn, 2008), http://naproche.net/downloads.shtml
7. VeriMathDoc website: http://www.ags.uni-sb.de/∼afiedler/verimathdoc/
8. Zinn, C.: Understanding Informal Mathematical Discourse, PhD thesis at the Uni-
versity of Erlangen (2004), http://citeseer.ist.psu.edu/233023.html