Extraction of Logical Structurefrom Articles in Mathematics ?
Koji Nakagawa1 , Akihiro Nomura2 , and Masakazu Suzuki1
1

Faculty of Mathematics, Kyushu University,
Kyushu Univ. 36, Fukuoka, 812-8581 Japan{nakagawa,suzuki}@math.kyushu-u.ac.jp,
2
Graduate School of Mathematics, Kyushu University

Abstract. We propose a mathematical knowledge browser which helps
people to read mathematical documents. By the browser printed mathematical documents can be scanned and recognized by OCR (Optical
Character Recognition). Then the meta-information (e.g. title, author)
and the logical structure (e.g. section, theorem) of the documents areautomatically extracted.
The purpose of this paper is to show the extraction method of logicalstructure specialized for mathematical documents. We implemented thismethod in INFTY which is an integrated OCR system for mathematical
documents. In order to show the effectiveness of the method we madea correct database from an existing mathematical OCR database, andmade an experiment.

1

Introduction

Computers became indispensable devices for mathematics. This phenomenon canbe seen by the success of mathematical systems (e.g. Mathematica, Maple) whichhave been being used for various other fields such as physics and economics.
In order to apply mathematics to the real world, mathematical knowledge
should be stored in computers in a way that people can easily use. Even if more
and more mathematics is done in formal ways, most of mathematical knowledge
is still stored in papers or books. Therefore digitizing mathematical text is still
important.
1.1

Levels of Digitization

There are several kinds of mathematics digitization. Adams gave some classifications of digitization of mathematics[1]. Based on this consideration, in thispaper we introduce five levels of mathematics digitization.
– level 1: bitmap images of printed materials (e.g. GIF, TIFF),?

This work is (partially) supported by Kyushu University 21st Century COE Program, Development of Dynamic Mathematics with High Functionality, of the Ministry of Education, Culture, Sports, Science and Technology of Japan.

2– level 2: searchable digitized document (e.g. PS, PDF),– level 3: logically structured document with links (e.g. HTML, MathML,LATEX),– level 4: partially executable document (e.g. Mathematica, Maple),– level 5: formally presented document. (e.g. Mizar[6], OMDoc[4])Currently most of mathematical knowledge is stored and used mainly inprinted materials (level 1) such as books or journals. For being used actively it
is preferable that mathematical text is stored in a possibly higher level of digitization. However since making documents digitized to a higher level needs quite a
lot of efforts, digitization of mathematical knowledge has not been enhanced sofar. Therefore we definitely need software in order to automatize the digitization
process in a possibly higher level.
1.2

Technologies for Automatization

The automatization can be achieved step by step:– level 1 to level 2: OCR (Optical Character Recognition),
In order to retrieve searchable digitized document from bitmap images, OCR
is used. With OCR, character sequences can be recognized from bitmap images and then they can be used for searching words. Especially recognition ofmathematical formulae is the most important in recognizing mathematical
documents. The mathematical formulae recognition has been well investigated, e.g. [8].
– level 2 to level 3: Extracting Logical Structure and Hyper Links,
Obtained data after OCR are basically characters having positions in a pagestructured by lines and areas. They do not directly contain meta-information(e.g. author, title) of a paper and structural information (e.g. section, subsection). Also they do not have hyper links which point to internal and external
documents.
– level 3 to level 4: Semantics Recognition from Presentation,
Sometimes executable blocks (e.g. mathematical expressions, algorithms) appear in mathematical text. In level 3 mathematical expressions are describedin a two-dimensional (presentational) way. We need to extract semantic expressions from these presentational expressions. Mathematica[10] has standard collections of these transformation rules which retrieve semantics ofpresentational expressions and one can even define their own style of notation (See MakeExpression function in [10]).
– level 4 to level 5: Understanding Mathematical Document,
Usually mathematical statements such as definitions, lemmata, theorems,
and proofs are written in natural languages in books or papers. Therefore
for treating them in computers we need natural language processing. The
first step of the natural language processing is parsing. For parsing it iscommon to make a corpus which is a set of grammar rules extracted fromused expressions. Making a corpus for mathematical statements was achieved

3

by Baba and Suzuki[2]. After parsing, formalizing written mathematical description to logical formulae in a predicate logic can be achieved. Formalizedstatements can be used for proving in computers by theorem provers suchas Theorema[3].
Since current our mathematical activities range over all digital levels, weneed software which covers these all technologies from scanning to proving ina coherent manner. The ultimate goal is that scanned mathematical papers areprocessed and the software system gives us whether proofs are correct, though
this goal is very ambitious.
Since the ultimate goal is quite ambitious, as a sub-goal we propose a mathematical knowledge browser which covers from level 1 to level 3 in Section 2.
In order to make such a browser, some technologies are necessary. One of thetechnologies is to extract logical structure from documents after OCR. In Section 3 we discuss the method of extracting logical structure from mathematical
documents. In order to show the effectiveness of the method, we made a correct
database which can represent logical structure information based on an existing
mathematical database for OCR, and experimented for the correct database. In
Section 4 the correct database is described and the experimental result will beshown. Then we conclude the discussion in Section 5.

2

Mathematical Knowledge Browser

The mathematical knowledge browser helps people to do mathematics from level
1 to level 3. One of inputs for this mathematical knowledge browser is a printed
mathematical document. A printed document can be scanned, and then processed by OCR. After OCR logical structure and hyper links are automaticallyextracted and shown to users.
We will implement this mathematical knowledge browser on an integrated
OCR system for mathematical documents called INFTY[8] (INFTY can be
downloaded3 ). INFTY reads scanned page images of a mathematical document
and provides their character recognition results. One of the distinguished characteristics of INFTY is that it can recognize two-dimensional mathematical expressions. INFTY has a graphical user interface which can show mathematicalexpressions in the ordinary two-dimensional mathematical notation, and has amanual error correction interface. The recognition results can be saved in various
formats, e.g. XML (called KML), HTML, LATEX, Mathematica, and braille.
2.1

User Interface

The browser consists of three panes: structure pane, reference pane, browsing
pane (Fig. 1). In the structure pane located in the left side, structural informationis shown as a tree like a file manager. The browser pane on the right bottom andthe reference pane on the right top show mathematical text. By clicking a link3

http://infty.math.kyushu-u.ac.jp/index-e.html

4Fig. 1. Screen Image of Mathematical Knowledge Browser (Sketch)in the browser pane, the text pointed by the link will be shown in the reference
pane so that people won’t lose the attention in the browser pane. For example,
by clicking the link ‘Lemma 2.1’ the reference pane shows ‘Lemma 2.1’ while thebrowser pane does not change.

2.2

Showing Relationship of Mathematical Theory Structure

Usually in a mathematical paper, mathematical components (e.g definitions,lemmata, theorems) have dependencies and one can construct a graph whichshows the dependencies. With the mathematical knowledge browser one can see
such dependency graphs. Fig. 2 shows an example of such a graph. For example,
suppose ’Lemma 3.1’ is used in the proof of ’Theorem 4.2’, the text ’Lemma 3.1’
should appear in the proof of ’Theorem 4.2’. From this fact we can detect thedependency automatically. By this functionality, readers can recognize theory
structure of a paper before reading into details.
Theorem 4.2
Lemma 3.1
Lemma 2.1
Lemma 2.2
Lemma 3.2
Fig. 2. Graph of Theory Dependency

5

Of course, showing theory structure is not a new idea. However the important point is that theory structure can be automatically extracted from printed
mathematical documents.

3

Extracting Meta-Information and Logical Structure

For realizing the mathematical knowledge browser, we need several technologies.
One of the technologies is to extract meta-information and logical structurefrom mathematical documents. In this section, we discuss the method to extract
automatically meta-information and logical structure.
There are several studies of logical structure extraction from documents.
Extensive surveys can be found in papers[5, 7]. In these studies target documents
vary from general documents to specific documents. The work presented in thispaper is unique because it is specialized for mathematical documents and it
extracts mathematical specific components (e.g. Theorem, Proposition). The
method proposed in this paper does not need to know layout styles beforehand,
while some other studies do.
3.1

Data Representation for Meta-Information and Logical
Structure

INFTY[8] produces the following nested structure as output from scanned images
as input.
– 1st page (size and position in the page)• 1st area (size and position in the page)∗ 1st line (size and position in the page)· 1st character (code, size and position in the page)· 2nd character (code, size and position in the page)· ...
∗ 2nd line
∗ ...
• 2nd area
∗ 1st line
· 1st character
· ...
∗ ...
– 2nd page
– ...
A document contains several pages and each page contains several areas whichhave positions and sizes in the page. An area can contain lines which also havetheir positions and sizes. A line has recognized characters with positions, sizes
and font styles.
INFTY produces output in a XML format called KML. We extended theKML format so that it can represent meta-information and logical structure.

6

For example, Fig. 3 shows a result output in the extended KML for a scanned
image shown in Fig. 4. The top element is ‘Doc’ which contains some ‘Sheet’
elements representing pages. A ‘Sheet’ element contains some ‘Area’ elements
whose positions and sizes are indicated by ‘rect’ attributes. The value of the‘rect’ attribute "lef t,up,right,down" indicates the positions of left, up, right,
down borders of the rectangle. An ‘Area’ element contains a ‘Text’ element
having a ‘Field’ element. A ‘Field’ element has several ‘Line’ elements whichhave again several ‘Char’ elements.
For the need of putting additional information for meta-information andlogical structure we added the ‘tag’ attribute for the ‘Text’ element in orderto represent the type of the text field. The values of the ‘tag’ attribute are‘PageHeader’, ‘PageNumber’, ‘Caption’, ‘Title’, ‘AuthorInfo’, ‘AbstractHeader’,‘Abstract’, ‘Keywords’, ‘Heading1’, ‘Heading2’, ‘Heading3’, ‘Heading4’, ‘Heading5’, ‘Text’, ‘ReferenceItem’, ‘Definition’, ‘Axiom’, ‘Theorem’, ‘MainTheorem’,‘Proposition’, ‘Corollary’, ‘Lemma’, and ‘Footnote’.
3.2

Extraction Algorithm

The algorithm of extracting meta-information and logical structure works in two
steps: segmenting areas in a page and putting appropriate tags to the areas. In
Fig. 4, areas are indicated by gray rectangles and their tags are put beside therectangles. An area can be either a special text area (page number, running
header, captions of tables and figures, footnotes, and headings) or a normal text
area which can be a mathematical component (e.g. theorem, definition). Laterthe method to extract mathematical components is described in details. After thecorrect process of putting tags, the conversion to a logically structured format(e.g. HTML, OMDoc) is straightforward.
Segmentation Segmentations can be done in the following three ways:– Segmentation by Spacing
By using spacing information, scanned images are separated into several
areas which can be either text areas, figure/table areas, or formulae areas.
– Segmentation by Style Difference
For each text area, the average size of the characters contained in the area
is calculated. The size of a character can be determined by the height ofthe character. Also boldness can be calculated by the horizontal width ofa character. In an area when the styles (bold, italic, and size) of lines are
obviously different from those of other lines, they are separately segmented.
– Segmentation by Keywords
In an area, when a special keyword of mathematical components (e.g. Theorem, Lemma, Definition) comes in the beginning of a line, basically the area
is segmented before the line. However sometimes there are cases that keywords do not indicate beginnings of mathematical components. This issue
will be discussed in the next subsection.

7<Doc version="1.1" language="English" ...>
<Sheet id="1" doc_file_name="Arkiv_1997.kml"
image_file_name="Arkiv_1997_185.tif" height="4438" width="3015" ...>
<Area rect="148,129,1801,266" id="1" ...>
<Text rect="148,129,1801,266" tag="PageHeader" ...>
<Field base_char_size="16,30,13,41" sub_char_size="11,20,9,28"><Line id="1" rect="148,129,1086,195"><Char code="0141" rect="148,133,195,180" ...>A</Char><Char code="0172" rect="200,151,223,180" ...>r</Char>...
</Line><Line id="2" rect="149,200,1801,266">...
</Area><Area rect="279,948,3022,1239" id="2" ...>
<Text rect="279,948,3022,1239" tag="Title" ...>...
</Area>...
</Sheet><Sheet id="2" doc_file_name="Arkiv_1997.kml"
image_file_name="Arkiv_1997_186.tif" height="4432" width="3002" ...>
<Area rect="229,169,326,215" id="1"><Text rect="229,169,326,215" tag="PageNumber" ...>
<Field base_char_size="16,28,12,39" sub_char_size="11,19,8,26"><Line id="1" rect="229,169,326,215">...
</Text></Area><Area rect="1088,168,2358,228" id="2"><Text rect="1088,168,2358,228" tag="PageHeader" ...>
<Field base_char_size="16,29,12,40" sub_char_size="11,20,8,27"><Line id="1" rect="1088,168,2358,228">...
</Area><Area rect="231,405,3224,701"><Text tag="Theorem"><Field><Line id="1" rect="392,405,3224,486"><Char code="2154" rect="392,410,452,467" bold="1"...>T</Char><Char code="2168" rect="458,409,506,467" bold="1"...>h</Char>...
</Area><CharInfo>... </CharInfo></Doc>
Fig. 3. Example of KML Output from INFTY OCR Engine

8Fig. 4. Example of Scanned Image Separated by Areas

9

Putting Tags to Areas After the segmentation process, appropriate tags are
put to these segmented areas. Here we describe criteria to decide appropriate
tags for areas.
– Title and Headings (e.g. section, subsection)
In order to put tags to these area, areas are ordered by the following lexicographic ordering through a document.
hSize, AllCapital, HCapital, Bold, Italici
Size:average size of characters contained in the area
AllCapital: true if all characters are written in capital (e.g. SYSTEM)
HCapital: true if only head characters are written in capital (e.g. System)
Bold:true if characters are written in bold
Italic:true if characters are written in italic
The ‘Title’ tag is put to areas appeared in the upper part of the first pageand is written in the largest area according to the lexicographic ordering
above. Headings usually start from either some numbers separated by periods
or special keywords like ‘Introduction’, ‘References’, ‘Bibliography’ in anemphasized (large/bold/italic) font. The tags ‘Heading1’,‘Heading2’, · · · are
put to the second, third, · · · largest areas in the lexicographic order.
– Author Information
The tag ‘AuthorInfo’ is put to areas which come next to the title before
headings or the abstract.
– Page Header, Footnote, and Page Number
The ‘PageHeader’(‘Footnote’) tag is put to areas positioned in the top (bottom) of pages and written in smaller fonts than the average font size of text
areas in a paper. The ‘PageNumber’ tag is put to areas which appear on
the bottom or upper right or upper left of a page and consist of numbers in
Arabic style or in Roman style (e.g. i, ii, iii, and iv).
– Mathematical Components (e.g. definition, lemma, theorem)
The tags for mathematical components are put to areas which start from thespecial keywords such as ‘Theorem’ and ‘Definition’. Here the problem is thatthese special keywords do not always indicate beginnings of mathematicalcomponents. The problem will be discussed in the next subsection.

3.3

Two Difficulties in Extraction of Mathematical Components

Correct extraction of mathematical components are important for further processing of mathematical documents, e.g. indexing, construction of dependency
graphs, and understanding of mathematical statements. Here we describe two
difficulties for extracting mathematical components.

10

Fig. 5. Looking for Beginnings of Mathematical Components

Looking for Beginnings of Mathematical Components Basic idea of detecting beginnings of mathematical components is to look for special keywords(e.g. Theorem, Lemma, and Definition). However these special keywords do notalways indicate beginnings of mathematical components.
For example in Fig. 5, the 6th line starts with the keyword ‘Proposition’,but it is not the beginning of a proposition declaration. It appears in text inorder to refer the ‘Proposition 3.4’ defined above. In Fig. 5 proposition components start from the keyword with all capital characters ‘Proposition’ which
distinguish from other keywords like ‘Proposition’. However we can not assume
that keywords of beginnings are written in all capital characters, because there
are many other papers which have different styles. Therefore we need a generalalgorithm in order to detect styles of mathematical components. In Section 3.4
the method will be described in details.

Looking for Endings of Mathematical Components Looking for endingsof mathematical components is not so easy task. For example, in Fig. 6, the fifthline is the ending of the lemma. In this case, the lemma is written in italic till thefifth line and from the sixth line it turns into normal font. Therefore the endingof the lemma can be detected. It is usual that lemmata or theorems are written initalic. Of course we can not assume that these components are written in italic.
Additionally definitions usually are not written in italic. Another criterion canbe indentation or space between lines. In this paper, we simply look for thestyle change from italic to normal font for mathematical components except
definitions, and for definitions we look for indentation.
When a mathematical component spreads over more than one page, failure
detection of ‘PageHeader’, ‘Footnote’, ‘PageNumber’ causes failure of looking
for endings of mathematical components. Therefore detection of ‘PageHeader’,‘Footnote’, ‘PageNumber’ is very important.

11

Fig. 6. Looking for Endings of Mathematical Components
Line Feature
Explanation
BK-Definition The line begins from the keyword ‘Definition’.
BK-Theorem
The line begins from the keyword ‘Theorem’.
BK-Proposition The line begins from the keyword ‘Proposition’.
BK-Corollary The line begins from the keyword ‘Corollary’.
BK-Lemma
The line begins from the keyword ‘Lemma’.
K-Italic
The keyword is written in italic.
K-BoldThe keyword is written in bold.
K-LCapital
All characters of the keyword are in large capital. (e.g PROPOSITION)
K-SCapital
Most of characters of the keyword are in small capital. (e.g. Proposition)
Indented
The line is indented.
Table 1. Line Features

3.4

Algorithm for Detecting Styles of Mathematical Components

In a paper, for a mathematical component the formatting style is uniform inprinciple. The idea of the algorithm for detecting styles of mathematical components is to use the style uniformity of a mathematical component.
The algorithm for detecting styles of mathematical components is describedin Fig. 7. At first features shown in Table 1 are extracted from lines, and thenfor each line two style values ‘lineDefStyle’ and ‘lineCompStyle’ are calculated.
The variable ‘lineDefStyle[i]’ stores the style value of the ith-line and is for
detecting the beginning of a definition mathematical component. The variable‘lineCompStyle[i]’ is for detecting other mathematical components, since mostof the cases styles of mathematical components except definitions are the same.
If the line does not start from a special keyword of mathematical components,
the style value becomes ‘-1’ which means that it can not be the beginning of amathematical component. Then the most frequent style values in a paper decide
the styles of beginning lines of mathematical components and the style values
are assigned to the variables ‘defStyle’ and ‘compStyle’. Finally when the stylevalue of a line is not ‘−1’ and it coincides with the most frequent value, the lineis the beginning of a mathematical component and the process of looking for theending is executed.

12// calculating the style value for each line
for i=1 to number_of_lines(paper) {lf=extract_features(paper.line[i]) // extracting line features// The number ‘-1’ means that the line can not be// the beginning of a mathematical component.
lineDefStyle[i]= if(lf.BK-Definition, stylefunc(lf), -1);
lineCompStyle[i]=if(lf.BK-Theorem || lf.BK-Proposition ||lf.BK-Corollary || lf.BK-Lemma, stylefunc(lf), -1);}// detecting most frequent style values
defStyle =most_frequent(lineDefStyle);
compStyle=most_frequent(lineCompStyle);// looking for endings
for i=1 to number_of_lines(paper){if(!(defStyle==-1) && lineDefStyle[i]==defStyle) {segmentArea();
look_for_ending_by_Indent(i);}if(!(compStyle==-1)&& lineCompStyle[i]==compStyle) {segmentArea();
look_for_ending_by_Italic(i);}...
};int styleFunc(LineFeatures lf){ return (lf.K-Italic*2^0+lf.K-Bold*2^1+lf.K-LCapital*2^2+lf.K-SCapital*2^3+lf.Indented*2^4); }...
}Fig. 7. Algorithm for Detecting Styles of Mathematical Components

4

Experiment

In order to see the effectiveness of the algorithm we made an experiment for acorrect database.
4.1

Outline of Database

We added new information for logical structure to a large-scale database ofmathematical documents[9, 8] and made the correct database which can be used
for the experiment. The documents contained in the database are 29 English
articles on pure mathematics (issued in 1970 - 2000). Basically for each journal
two old and new papers are selected. The numbers of pages and characters in the
database are 422 and 706,279, respectively. This database is larger than otherdatabases used in the past researches on math-OCR.
All pages were scanned in 600 dpi and binarised automatically by the samecommercial scanner (RICOH imagio Neo 450). The quality of resulting page images are noisy and include a lot of abnormal characters, such as touching char-

13
TagNameCorrect Success Begin- EndTagErr Miss- Rate1 Rate2
AreaErr AreaErr
Recog. (%)(%)
PageHeader
425
418
1
3
3
0
98.4
98.4
398
381
11
0
6
0
95.7
95.7
PageNumber
Title
28
27
0
1
0
0
96.4
96.4
AuthorInfo
28
23
1
3
1
0
82.1
82.1
126
113
2
1
10
0
89.7
89.7
Header1
Header2
14
13
0
1
0
0
92.9
92.9
Footnote
16
10
5
0
1
0
62.5
62.5
Definition
31
24
3
4
0
0
77.4
77.4
116
103
6
6
1
2
88.8
90.5
TheoremMain theorem
2
2
0
0
0
0
100.0 100.0
Proposition
91
83
5
3
0
0
91.2
91.2
Corollary
36
31
3
0
2
2
86.1
91.7
Lemma
107
92
8
6
1
2
86.0
87.9
Total
1418
1320
45
28
25
6
93.1
93.5
‘Correct’number of areas in the correct database.
‘Success’
number of success tagging by the method proposed in this paper.
‘Begin-AreaErr’ number of errors to detect beginnings of areas.
‘End-AreaErr’ number of cases which detected beginnings of areas,
but failed to detect endings of areas.
‘TagErr’
number of errors that different tags were put.
‘Miss-Recog.’ number of miss-recognitions by OCR for the special keywords.
‘Rate1’success rate computed by Success/Correct ∗ 100.
‘Rate2’success rate computed by (Success + Miss-Recog.)/Correct ∗ 100.
Table 2. Experimental Result

acters and broken characters. The maximum and minimum abnormal character
rates, which represent the quality of images, are 12.6% and 0.11%, respectively.

4.2

Experimental Result

We implemented the algorithm within the INFTY system and compared withthe correct database described above. The result is summarized in Table 2. When
there are miss-recognitions of characters, the keywords used for detection are noteffective for looking for beginnings of mathematical components. Therefore it isconsidered that ‘Success’+‘Miss-Recog.’ approximates the real success numbers
for the method described in this paper.
Main reason of the failures in detecting mathematical components is that themethod fails to detect endings of mathematical components because of the simple
ending detection method. Improving the method will improve the recognition
rate.

14

5

Conclusion

A method of extracting meta-information and logical structure from mathematical documents was presented and implemented on the base of the INFTY system.
In order to show the effectiveness of the method, we made an experiment and therecognition rate was 93.1% in the practical situation including miss-recognitionsof characters by OCR. We are now increasing the number of papers containedin the correct database in order to experiment for larger amount of papers.
The improvement of the recognition accuracy can be achieved by giving additional information to the system. For example, knowing journal names, which
may be automatically extracted from running headers, can contribute to the accuracy, because a journal has its own format. Also when the system fails to detect
logical structure, a little human interaction can contribute to the accuracy.
With the facility of automatic linking, we will be able to implement the mathematical knowledge browser based on the INFTY system. The mathematicalknowledge browser can be extended to a system for editing mathematical documents. With the editor one can input mathematical statements in formalized
formulae. The formalized formulae can be sent to computing, solving, proving
services located in the Internet and the results can be obtained. Namely it canbe used as a front-end for mathematical services. We expect this mathematicalknowledge browser to become a digitalization tool for mathematics, and enhancemathematical activities.

References
1. A. A. Adams. Digitisation, Representation and Formalisation: Digital Libraries ofMathematics. In Mathematical Knowledge Management (MKM 2003), Feb. 16th 18th, 2003, Bertinoro - Italy, LNCS 2594. Springer, 2003.
2. Y. Baba and M. Suzuki. An Annotated Corpus and a Grammar Model of Theorem
Description. In Andrea Asperti, Bruno Buchberger, and James Harold Davenport,
editors, Second International Conference, MKM 2003, Bertinoro, Italy, pages 93–
104, Feb. 2003.
3. B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and
W. Windsteiger. The Theorema Project: A Progress Report. In Symbolic Computation and Automated Reasoning, pages 98–113. A.K. Peters, 2001.
4. M. Kohlhase. OMDoc: An Infrastructure for OpenMath Content Dictionary Information. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic
Manipulation), 34(2):43–48, 2000.
5. S. Mao, A. Rosenfeld, and T. Kanungo. Document Structure Analysis Algorithms:
A Literature Survey. In Document Recognition and Retrieval X, number 5010 inProceedings of SPIE, pages 197–207, January 2003.
6. P. Rudnicki. An Overview of the Mizar Project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992. http://mizar.org.
7. K. M. Summers. Automatic Discovery of Logical Document Structure. PhD thesis,
Cornell University, 1998.

15
8. M. Suzuki, F. Tamari, R. Fukuda, S. Uchida, and T. Kanahori. INFTY — An
Integrated OCR System for Mathematical Documents. In ACM Symposium on
Document Engineering (DocEng ’03), Grenoble, France, Nov. 20-22, 2003.
9. S. Uchida, A. Nomura, and M. Suzuki. Quantitative Analysis of Mathematical
Documents. Submitted to a journal.
10. S. Wolfram. The Mathematica Book, Fifth Edition. Wolfram Media, Inc., 2003.