MathML Conference 2002: Presentations

Formal Mathematical Proof Explanations in Natural Language Using MathML: An Application to Proofs in Arabic

Hanane Naciri and Laurence Rideau
INRIA Sophia Antipolis

Abstract

When developing formal mathematical proofs on the computer, dissemination of the proofs is an important part of their life cycle. And nowadays, the Internet is a necessary medium for this.

There is the choice between communicate the compiled form of the proof (a lambda-term representing the proof term, as in the HELM project [3]), or the script source of the proof (the set of commands given to the proof engine to perform the proof). However, neither the compiled form nor the script can easily be understood by non-specialists. Another possibility is to communicate natural language explanations [2], which are automatically generated from the previous forms. These explanations must look like mathematical proofs written by mathematicians, so that they can be understood by people who are not familiar with theorem provers.

All these forms (lambda-term, command script or natural language explanation) mix text and mathematical formulas, so XML including MathML for formulas is a good candidate to enable the communication of such proofs on the Internet.

To get new tools for theorem provers, we have studied how to generate natural language explanations from lambda-terms and proof scripts. Note that these natural language explanations can also be generated from incomplete proofs and used by the user during his proof development (see Figure 1).

Figure 1: A PCOQ session with Arabic proof explanations.

First, we have experimented with displaying the generated mathematical documents in English or French, where text and mathematics are written from left-to-right. For that purpose we have developed our own display library FIGUE [5], which allows both text display and 2-dimensional display for mathematics. To get a standard Web output, we also have developed a translator from our own format to MathML-content [6], allowing the display of our proofs by any MathML-compliant browser.

The next challenge is to display Arabic proof explanations, where the text follows the Arabic direction (from right-to-left), and the mathematical formulas are written from left-to-right (as is done in Morocco) or from right-to-left (as is done in Egypt). This involves:

understanding precisely the various methods used to display mathematics in Arabic languages;
extending our display library FIGUE, originally dedicated to left-to-right display, to allow right-to-left display;
extending FIGUE to mix directions display in the same document: for example Arabic text including mathematical formulas (which may eventually include Arabic text);
studying the MathML behavior in a bidirectional context;
extending our translator from FIGUE format to MathML, to process our Arabic proof explanations.

The first three topics already have been studied and the extended version of FIGUE, supporting the bidirectional display, has been tested in the PCoq interface (a graphical interface for the Coq proof assistant [4]), allowing Arabic proof explanations¹ as shown in Figure 1. The top part of this window is an area containing the proof commands, whereas the bottom part contains Arabic explanations generated from these commands.

The two last topics (related to MathML) are currently being studied. According to our FIGUE experiment, new display rules and a new bidirectional algorithm for MathML are proposed to address right-to-left or bidirectional layout of mathematical formulas. Web browsers which support MathML will then be able to support more languages to disseminate scientific documents on the Internet. Figure 2 shows how Mozilla displays an XHTML (including MathML) document, which is generated from the Arabic proof explanation shown in Figure 1. The text direction is controlled via XHTML markup (which adopts the Unicode bidirectional algorithm [1]). All mathematical formulas which are represented in MathML have the same direction (left-to-right).

Modern mathematical formulas have been introduced in Arabic countries through Latin languages (English or French). In order to adopt these formulas to Arabic languages two different choices have been made: either write the formulas from right to left, with mirrored symbols (as is done in Egypt and Syria), or write the formulas from left to right (as is done in Morocco and Algeria), which makes translation easier from Latin languages but involves the mixing of directions in the same document. Currently, Arabic countries tend to choose the second method and rather use the standard mathematical notations.

MathML does not yet address mathematical formulas written from left to right but including right-to-left text, or mathematical formulas written from right-to-left following the Arabic text direction (case of Egyptian mathematical formulas). In the last case, several mathematical symbols or characters are mirrored and some mathematical elements have a non-standard behavior (for example, matrix terms are oriented from right to left). Note that there are some cases where it is necessary to indicate the direction of the mathematical text in Arabic document in order to have an non-ambiguous display: for example, the mathematical expression A - B can be read in two different ways (left-to-right or right-to-left) with two different meanings.

Figure 2: Mozilla display of an XHTML document generated from FIGUE. Text is right-to-left, but mathematical formulas are left-to-right.

References

[1]: The Bidirectional Algorithm. http://www.unicode.org/unicode/reports/tr9/bidi.
[2]: Y. Coscoy. A natural language explanation for formal proofs. In Springer-Verlag LNCS/LNAI, editor, Proceedings of the Int. Conf. on logical Aspects of Computational Linguistics (LACL), volume 1328, Nancy, September 1996.
[3]: Helm project, http://www.cs.unibo.it/~asperti/helm/home.htm.
[4]: G. Huet, G. Kahn, and C. Paulin-Mohring. The coq proof assistant : A tutorial : Version 6.1. Technical Report RR-0204, INRIA, Decembre 1997.
[5]: H. Naciri and L. Rideau. Figue: Mathematical formula layout with interaction and mathml support. In Proceedings of the Fifth Asian Symposium on Computer Mathematics ASCM'2001, Matsuyama, Japan, September 2001. Ehime University.
[6]: H. Naciri and L. Rideau. The mariage of mathml and theorem proving. In Proceedings of the IAMC'2001 Workshop on Internet Accessible Mathematical Computation in connection with ISSAC'2001, Western Ontario Canada., July 2001. http://icm.mcs.kent.edu/research/iamc.html.

1

The English explanation corresponding to the same proof:

Let us prove .

Let n be an element of N.

By induction on n:

-Case 0: Find a proof of 

-Case (s): Find a proof of .