The Naproche CNL [2] is a controlled natural language for mathematical texts, i.e. a controlled subset of the semi-formal language of mathematics (SFLM) as used in mathematical journals and textbooks. The Naproche system translates Naproche CNL texts first into Proof Representation Structures (PRSs, [2]), an adapted version of Discourse Representation Structures, which are further translated into lists of first-order formulae which are used for checking the logical correctness of a Naproche text using automated theorem provers. The two main applications that we have in mind for Naproche are to make formal mathematics more readable to the average mathematician, and to use it as a tool that can help undergraduate students to learn how to write formally correct proofs and thus get used to (a subset of) SFML. A recent addition to the Naproche CNL is the possibility to make plural statements. By this we mean not only statements involving nouns in the plural (e.g. “numbers”) and verbs conjugated in plural forms (e.g. “are”), but also conjunctions of noun phrases (e.g. “x + y and x · y are even”). We discuss the collective-distributive ambiguity as well as a special scope ambiguity conjunctions give rise to, and explain how these ambiguities are resolved in Naproche. Plural definite noun phrases (e.g. “the real numbers”) are not yet implemented in Naproche and are left out of the discussion in this abstract.
The following sentence is ambiguous:
(
It can mean either that three men lifted a piano together (in a single lifting act), or that there were three lifting acts, each of which involved a different man lifting a piano. The first is called the collective reading, the second the distributive reading. The ambiguity arises because the agent of a lifting event can either be a collection of individuals or a single individual.
In SFLM, both the collective and the distributive reading exist:
(
Instead of (
Since “prime number” expresses a unary relation, it is not possible to group
two of its logical arguments into a single linguistic argument; this explains why
(
We know of no example where a mathematical expression has a linguistic
argument that can be either a collectively interpreted plural NP or a singular
NP (and can hence also be a distributively interpreted plural NP), and could
therefore give rise to an ambiguity like that of (
Another kind of ambiguity of special interest for our treatment of plurals and
noun phrase conjunctions is a scope ambiguity that arises in certain sentences
containing a noun phrase conjunction and a quantifier:
(
The conjunction scope can be disambiguated semantically as in (
In general, there is a strong tendency in SFLM texts to resolve scope
ambiguities by giving wider scope to a quantifier that is introduced earlier in a sentence
than to a quantifier introduced later in the sentence. This is a principle that we
have already long ago adopted into Naproche in order to avoid scope ambiguities
in the Naproche CNL. With the addition on NP conjunctions and disjunctions,
we extended this principle to their scopes, with the exception of the cases like
(
In SFLM texts, one often sees sentences like (7) and (8), which are interpreted in a pairwise way as in (9) and (10): (7) 7, 12 and 25 are coprime. (8) All lines in A are parallel. (9) coprime(7, 12) ∧ coprime(12, 25) ∧ coprime(7, 25) (10) ∀x, y ∈ A (x 6= y → parallel(x, y))2 Sometimes, especially in connection with the negative collective adjectives “distinct” and “disjoint”, this interpretation is reinforced through the use of the word “pairwise”, in order to ensure that one applies the predicate to all pairs of objects collectively referred to by the plural NP. But given that this pairwise interpretation is at any rate the standard interpretation of such sentences even in the absence of the adverb “pairwise”, we decided not to require the use of the word “pairwise” in the Naproche CNL.
The Naproche CNL allows only this pairwise interpretation for a plural NP that is used as a grouped argument of such a collective adjective.3 (11) is a sentence where another reading might naturally be preferred. However, it seems to us that such sentences hardly appear in real mathematical texts. (11) Some numbers in A and B are coprime.
of terms as in this example. One real example that we found comes from page 4 of [1]: “Notice that 13, 37, 61, . . . , are primes p such that p3 + 2 and p3 + 1 are squarefree.” 2 The distinctness condition here can be ignored in the case of symmetric relations like “parallel”, but is certainly needed for non-reflexive relations like “coprime” or “disjoint”. 3 Which adjectives classify as collective adjectives is coded into the lexicon of the
Naproche CNL.
The PRS construction algorithm for the representation of single sentences is similar to the standard threading algorithm for DRS construction (see [3]), and is implemented in Prolog. This algorithm has been adapted in order to cope with plurals, plural ambiguity resolution and pairwise interpretations as explained in the previous sections. We illustrate how the algorithm treats plurals by considering the following example sentence: (12) x and y are distinct primes p such that 2p + 1 is a square number and some odd prime divides x + y.
The algorithm works by first producing a preliminary representation (left PRS in Fig. 1): Here the NP conjunction gets a plural discourse referent (p in Fig. 1), which is linked to the discourse referents of the conjuncts by a plural dref condition. We give the NP conjunction wide scope over all quantifiers introduced later, and all assertions made in the scope of the plural NP are inserted in a special plural sub-PRS. Now a number of processes yield the final PRS: x, y, p plural dref(p,[x,y]) a, b, c distinct(p) prime(p) a = 2p + 1 plural(p, square(a) ) odd(b) prime(b) c = x + y divide(b,c) x, y, p, b, c plural dref(p,[x,y]) distinct(p) odd(b) prime(b) c = x + y divide(b,c)
a plural(p, apr=im2ep(p+) 1 square(a) ) x, y, b, c distinct(x, y) odd(b) prime(b) c = x + y divide(b,c) a1 prime(x) a1 = 2x + 1 square(a1) a2 prime(y) a2 = 2y + 1 square(a2) 1. In the plural sub-PRS, we mark every PRS conditions which consists of a predicate that has the plural discourse referent as grouped argument (“distinct(p)” in Fig. 1, marked by italicisation) 2. In the plural sub-PRS, we recursively mark (in Fig. 1 by underlining) all PRS conditions that weren’t marked in step 1 and contain the plural discourse referent or a marked discourse referent, and all discourse referents contained in a PRS marked in this way, until no more conditions and discourse referents can be marked by this process. 3. All discourse referents and PRS conditions in the plural sub-PRS not marked in step 2 get pulled out of the plural sub-PRS and inserted into its super-PRS (yielding the second PRS in Fig. 1).
The syntax of Attempto Controlled English (ACE) allows plurals, which are interpreted in ACE in an unambiguous way. The disambiguation used by ACE is very distinct from Naproche’s: while Naproche gives preference to distributive and wide-conjunction-scope readings, ACE allows only collective and narrowconjunction-scope readings, unless the word “each” is used. This difference is due to the fact that for Naproche we focused on the interpretations common in SFLM, whereas ACE took the English language as a whole into account. Our focus on mathematical language also made it important for us to give “x and y are coprime” and “x is coprime to y” the same representation, which ACE does not do.
ForTheL, the controlled natural language of the System for Automated Deduction (SAD), a project with similar goals to Naproche, already included the two uses of words like “parallel” and “to commute” and produced the same representation no matter in which way they were used [5].
At the moment, Naproche does not yet allow anaphoric pronouns like “it” and “they”. When Naproche is extended to allow them, some rules specifying how to control the many ways in which an anaphoric antecedent for “they” can be chosen (see [4]) will have to be specified and implemented, again with special attention to existing usage in SFLM.