Verification of Mathematical Formulae Based ona Combination of Context-Free Grammar andTree Grammar
Akio Fujiyoshi1 , Masakazu Suzuki2 , and Seiichi Uchida3
1

Department of Computer and Information Sciences, Ibaraki University
fujiyosi@mx.ibaraki.ac.jp
2
Faculty of Mathematics, Kyushu University
suzuki@math.kyushu-u.ac.jp
3
Faculty of Information Science and Electrical Engineering, Kyushu University
uchida@is.kyushu-u.ac.jp

Abstract. This paper proposes the use of a formal grammar for theverification of mathematical formulae for a practical mathematical OCR
system. Like a C compiler detecting syntax errors in a source file, we wantto have a verification mechanism to find errors in the output of mathematical OCR. Linear monadic context-free tree grammar (LM-CFTG)
was employed as a formal framework to define “well-formed” mathematical formulae. For the purpose of practical evaluation, a verification
system for mathematical OCR was developed, and the effectiveness ofthe system was demonstrated by using the ground-truthed mathematical
document database INFTY CDB-1.

1

Introduction

Grammatical analysis is useful for many types of verification problems. For example, a C compiler grammatically analyzes a source file and returns error messages with the location and type of errors. For mathematical OCR [1], it isnatural to think that such grammatical analysis helps to detect misrecognitionsof characters and structures in mathematical formulae. This paper proposes amathematical-formulae verification method for a practical mathematical OCR
system based on a combination of context-free grammar [2] and tree grammar [3].
Grammatical analysis can be classified into two levels: syntactic analysis
and semantic analysis. This paper concentrates only on the syntactic analysis
of mathematical formulae because we wanted to build a very fast verification
system. Needless to say, semantic analysis is also very important for the improvement of mathematical OCR. However, we will leave this task for anothertime. We use the term “well-formed” to mean syntactic correctness. Since syntactic correctness doesn’t necessarily mean semantic correctness, we can consider
unsatisfiable formulae, e.g., “1+2 = 5”, and tautological formulae, e.g., “x = x”,
as “well-formed” formulae if they are syntactically correct.
The final aim of this study is to completely define “well-formed” mathematical formulae. In other words, we want to have a grammar to verify any

2

A. Fujiyoshi, M. Suzuki and S. Uchida

n

n

Σ

i

=

i

=

0

(

n

+

1

)

2

Scanned image
Tree representation

Fig. 1. A result of structural analysis of a mathematical formula

Exp
Sum

Σ

Exp
Frac

Init
Fan-out rules

Exp

Init

Exp = Exp

Term

FactorExp

Exp + Exp

FactorExp

Term

Factor

1n

Term

Term Term

Factor( Exp )

Context-free rules

Fig. 2. Some rules of the grammar

mathematical formula that has appeared, or will appear, in a long-term buildup of mathematical documents. There were other grammatical approaches to theverification of mathematical formulae such as [4–6]. The proposed verification
method will extend the coverage of those approaches.
In order to define “well-formed” mathematical formulae, we employed linear
monadic context-free tree grammar (LM-CFTG) [3] as a formal framework. As
shown in Fig. 1, a mathematical OCR system offers a tree representation of amathematical formula from a scanned image. Therefore, we needed a grammar
formalism to define a set of tree structures. An LM-CFTG defines a set of tree
structures by arranging fan-out rules and context-free rules, where fan-out rules
are used to describe the structural growth of a tree, and context-free rules areused to describe linear growth. For example, some fan-out rules and contextfree rules of the grammar defining “well-formed” mathematical formulae areillustrated in Fig. 2.
The proposed verification method allows us to build a very fast verification
system. Theoretically, the verification process of most mathematical formulae
will be completed in linear time depending on the size of the input, though some
exceptional mathematical formulae require cubic time. We need a very fast verification system because verification should be done for numerous recognition
candidates to improve the reliability of mathematical OCR. We experimentally
built a verification system and executed the system on the ground-truthed mathematical document database INFTY CDB-1 [7]. The verification of 21, 967 mathematical formulae (size: 48.1MB) was finished within 10 seconds by a PC (CPU:Pentium4 3.06GHz, RAM: 1GB).

Verification of Mathematical Formulae Based on Formal Grammar

3

The accomplishment of this very fast verification system mainly resulted fromthe following two features of the proposed verification method:– Division of a mathematical formula into sub-formulae; and– A grammar formalism with a fast recognition algorithm.
The idea of the division of a formula into sub-formulae is common to wellknown algorithm design paradigms such as “Divide and Conquer” and “Dynamic
Programming.” The employment of LM-CFTG enables us to use not only parsing
algorithms for LM-CFTG [8] but also well-established parsing techniques forcontext-free grammar (CFG) [2, 9].
Although the proposed verification method may be useful in general, thispaper mainly discusses the implementation of a verification system created to
be used with InftyReader [10]. The information about InftyReader and othersupporting software can be found on the Infty Project website [11].
This paper is organized as follows: In Section 2, the grammar defining “wellformed” mathematical formulae is explained; in Section 3, the outline of the
proposed verification method is described; in Section 4, the results of the experiment are shown; in Section 5, LM-CFTG is introduced as a formal framework
for the grammar defining “well-formed” mathematical formulae; and in Section
6, the conclusion is drawn and future work determined.

2“Well-Formed” Mathematical Formulae

In order to define “well-formed” mathematical formulae, linear monadic contextfree tree grammar (LM-CFTG) [3] was employed as a formal framework. The
definition and the formal properties of LM-CFTG will be introduced in Section 5. To choose an appropriate grammar formalism, it was necessary for agrammar formalism to have sufficient descriptive power to process a diversity ofmathematical formulae. In addition to descriptive power, we also required thata grammar formalism be accompanied by a very fast parser.
An LM-CFTG is defined by arranging fan-out rules and context-free rules.
Fan-out rules are used to define possible structural configuration of mathematical formulae. We should arrange them for symbols which are possibly connectedwith adjunct symbols. Examples of those symbols are “capital sigma” for summation, “capital pi” for product, “radical sign” for square root, “long bar” forfraction, “integral sign” for definite integral, etc. Because any variable may havea subscript, we arranged a fan-out rule for all italic alphabet symbols. Contextfree rules are used to define possible linear sequences of symbols of mathematicalformulae. Context-free rules constitute a context-free grammar (CFG) [2], andthus we can use well-established parsing techniques for CFG [9].
We experimentally developed a grammar defining “well-formed” mathematical formulae. The grammar consists of 35 fan-out rules and 170 context-freerules. The number of rules will be increased with the refinement of the grammar. A representative sample of the grammar is illustrated in the appendix at
the end of this paper.

4

A. Fujiyoshi, M. Suzuki and S. Uchida
Table 1. Grammatical categories
Category
Explanation and Example
Math Acceptable mathematical formula“u(a, b) = Int Frac”
Range Range of value of a variable“1 ≤ i ≤ n”
Init
Initialization of a variable“i = 0”, “i = k”
Exp
Acceptable expression“2 + 3”, “n(n + 1)”
ExpList List of expressions connected with signs“a < b < c < d”, “z = x + y”
Subscript Subscript of a variable“2”, “n”, “1, 2”, “1, 2, 3, 4”
Supscript Supscript of a variable and expression“0”, “00”, “2”, “n”, “1, 2”

On the development of the grammar, we tried to arrange context-free rules sothat they constitute a deterministic context-free grammar (DCFG) [2] because
we could take advantage of a linear-time parsing technique for DCFG [9]. Unfortunately, we needed to add some context-free rules, which break the conditionof DCFG, and this is the reason why a verification process of some exceptional
mathematical formulae requires cubic time. Most of those context-free rules are
related to the vertical-bar symbol because the usage of vertical bar is too diverse:
absolute value, divides, conditional probability, norm of a vector, etc.
Table 1 shows the grammatical categories defined by the context-free rulesof the grammar.

3

Outline of the Verification Method

In this section, we describe the outline of the proposed verification method. We
start with the input to the verification system, that is to say, the output ofmathematical OCR.
The output of InftyReader is given in InftyCSV format. An example of an
InftyCSV text expressing a mathematical formula is shown in Table 2. Eachline corresponds to a symbol in the formula, where: “ID” is the number uniquely
assigned to the symbol; “x1 , x2 , x3 , x4 ” are the coordinates of the rectangulararea; “Mode” is a flag showing if the symbol is a part of a mathematical formula;“Link” expresses the relationship with the parental symbol; “Parent” is the IDof the parental symbol; and “Code” is the internal character code of the symbol.
The original image and the rectangular representation of the formula are shownat (1) and (2) in Fig. 3.

Verification of Mathematical Formulae Based on Formal Grammar

5

Table 2. An example of an InftyCSV text
ID
1,
2,
3,
4,
5,
6,
7,
8,
9,
10,
11,
12,
13,
14,
15,
16,
17,

3.1

x1
1487,
1542,
1563,
1610,
1646,
1686,
1728,
1801,
1853,
1868,
1909,
1945,
1986,
1911,
1977,
1999,
2035,

y1
708,
685,
704,
732,
683,
685,
708,
624,
782,
622,
717,
629,
650,
736,
740,
757,
740,

x2
1535,
1559,
1603,
1622,
1679,
1703,
1780,
1858,
1881,
1891,
2053,
1985,
2016,
1967,
1994,
2029,
2051,

y2
766,
758,
742,
753,
742,
758,
724,
812,
810,
658,
722,
689,
689,
800,
813,
796,
813,

Mode
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,
1,

Link Parent Code-1,
-1,0x426C0,1,
0x19800,2,0x41610,
3,0x142C0,4,0x41620,
5,0x1981
0,
6,
0x1D3D
0,7,
0x33F02,8,0x41611,8,0x4162
0,
8,
0x33D15,11,0x41640,12,0x41636,
11,0x02480,
14,0x19800,15,0x41630,
16,
0x1981

Construction of a Tree Representation

First, the verification system converts an InftyCSV text into a linked list called atree representation. A node of a linked list is illustrated in Fig. 4. By preparing
nodes for all symbols and connecting them in accordance with “Link” and “Parent” information in an InftyCSV text, the tree representation of a mathematicalformula is constructed. The InftyCSV text in Table 2 is converted into the tree
representation shown at (3) in Fig. 3.
3.2

Division of a Mathematical Formula into Strings

Secondly, strings are extracted from a tree representation of a mathematicalformula. Strings are obtained by concatenating symbols horizontally connected
in a tree representation. From the tree representation shown in Fig. 3, thefollowing five strings are extracted:“u ( a , b ) = Int Frac”,
“b”,
“a”,
“d c”, and“Θ ( c )”.
3.3

Grammatical Analysis

Grammatical analysis is executed in two stages: linear sequence analysis andstructural inspection. In the linear sequence analysis, a parser for a context-free6

A. Fujiyoshi, M. Suzuki and S. Uchida(1) Original image

µ

(

a

,

(2) Rectangular representation

b

)

=

b

d

c

a

Θ

(

∫
c

)

(3) Tree representation

Fig. 3. The mathematical formulaupper
L _ supscript

R _ supscript
horizontal

L _ subscript

R _ subscript
underFig. 4. A nodegrammar (CFG) [2] is utilized, and, for each string extracted from a tree representation of a mathematical formula, the fitness to the grammatical categories is
examined. In Table 3, the fitness to the grammatical categories for the strings
is shown. The linear sequence analysis is the most time-consuming task in the
proposed verification method, and may cost cubic time depending on the size ofthe input in the worst case, while the other tasks can be done in linear time.
After the linear sequence analysis, the structural inspection takes place. In
the structural inspection, the connectivity of nodes is examined by searchingfor matching fan-out rules. The structural inspection process is illustrated inFig. 5. The connection of the adjunct strings, “b” and “a”, and the integral sign
are inspected. The connection of the adjunct strings, “d c” and “Θ ( c )”, andthe long bar are also inspected.
The mathematical formula in the example was successfully verified as a “wellformed” mathematical formula.

Verification of Mathematical Formulae Based on Formal Grammar

7

Table 3. Fitness to the grammatical categories
Strings
Math Rangeu ( a , b ) = Int Frac yes
yes
b
yes
yes
a
yes
yes
dc
yes
yes
Θ(c)
yes
yes

Init
yes
no
no
no
no

b

µ

(

a

)

b

,

=

Int

a

Exp ExpList Subscript Supscript
no
yes
no
no
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes
yes

c

d
Frac

Θ

(

c

)
Exp

Exp
Int

∫

Frac
Exp

Exp

Fig. 5. Structural inspection

4

Experimental Results

We experimentally built a verification system in accordance with the proposed
verification method. For implementation of the system, the program was written
in C language, and GNU Bison [12], a parser generator for CFG, was utilized.
For evaluation, we executed the system on the ground-truthed mathematical
document database INFTY CDB-1 [7].
The verification of 21, 967 mathematical formulae in INFTY CDB-1 (size:
48.1MB) was finished within 10 seconds by a PC (CPU: Pentium4 3.06GHz;
RAM: 1GB). The speed of the proposed verification method was experimentallyconfirmed. Theoretically, a verification process of most mathematical formulae
will be finished in linear time depending on the size of the input, though some
exceptional mathematical formulae require cubic time.
The verification system produces verification results in XHTML format with
MathML inclusions and displays error messages on a web browser such as Mozilla
Firefox [13]. An error message identifies the position and type of suspicious
mathematical-formula error as enlarged and colored red.
(1), (2), (3) and (4) in Fig. 6 are error messages produced by the verification system. Original images corresponding to the error messages are shown in
Fig. 7. As for (1), the verification system successfully detected the misrecognition of a comma before the letter ‘b’. The comma was misrecognized as a period.
With regard to (2), the verification system detected a faulty correspondence of8

A. Fujiyoshi, M. Suzuki and S. Uchida

(1)

(2)

(3)

(4)

Fig. 6. Error messages produced by the verification systemparentheses. Looking at the original image, we noticed that this was an error
from the original document. Concerning (3), the verification system successfully
detected the misrecognition of the angle bracket. The angle bracket was misrecognized as a less-than sign. And about (4), a structural error was detected sincea left parenthesis may not have a superscript. A portion of the left parenthesis
was misrecognized as a prime symbol.

5

Formal Framework

In this section, we introduce the formal definitions of tree and linear monadic
context-free tree grammar (LM-CFTG). LM-CFTG was employed as a formal
framework to define “well-formed” mathematical formulae. We also introduce
known results for LM-CFTG.
5.1

Tree

A ranked alphabet is a finite set of symbols in which each symbol is associatedwith a natural number, called the arity of a symbol. Let Σ be a ranked alphabet.
For n ≥ 0, let Σn = {a ∈ Σ | the arity of a is n}. A ranked alphabet is monadic
if the arity of each its element is at most 1.
The set of trees over Σ, denoted by TΣ , is the smallest set of strings overelements of Σ, parentheses and commas defined inductively as follows:Verification of Mathematical Formulae Based on Formal Grammar

9

(1)

(2)

(3)

(4)

Fig. 7. Original images(1) Σ0 ⊆ TΣ , and(2) if a ∈ Σn for some n ≥ 1, and t1 , t2 , . . . , tn ∈ TΣ , then a(t1 , t2 , . . . , tn ) ∈ TΣ .
Let x be a variable. TΣ (x) is defined as TΣ∪{x} taking the rank of x to be 0.
For t, u ∈ TΣ (x), t[u] is defined as the result of substituting u for the occurrencesof the variable x in t. A tree t ∈ TΣ (x) is linear if x occurs exactly once in t.
5.2

Linear Monadic Context-Free Tree Grammar

An linear monadic context-free tree grammar (LM-CFTG) is a four-tuple G =(N, Σ, P, S), where:– N is a monadic ranked alphabet of nonterminals,– Σ is a ranked alphabet of terminals, disjoint with N ,– S ∈ N0 is the initial nonterminal, and– P is a finite set of production rules of one of the following forms:(1) A → uwith A ∈ N0 and u ∈ TN ∪Σ , or(2) A(x) → u
with A ∈ N1 and a linear tree u ∈ TN ∪Σ (x).
For an LM-CFTG G, the one-step derivation ⇒ is the relation over TN ∪Σ (x)Gsuch that, for t ∈ TN ∪Σ (x), (1) if A → u is in P and t = t0 [A] for some linear

10

A. Fujiyoshi, M. Suzuki and S. Uchida

t′

t′
A

u

x

A

u

⇒
G

x

t ′′

t ′′

Fig. 8. One-step derivation
B
b

B
A

a

A
C

(1)

A

A

(2)

C

C1

x

x

Ci −1

x

Ci +1

Cn

x

(4)

(3)
Fig. 9. Chomsky-like normal form

tree t0 ∈ TN ∪Σ (x), then t ⇒ t0 [u], and (2) if A(x) → u is in P and t = t0 [A(t00 )]Gfor some linear trees t0 , t00 ∈ TN ∪Σ (x), then t ⇒ t0 [u[t00 ]]. See Fig. 8.
G∗Let ⇒ denote the reflexive transitive closure of ⇒ . The tree language genG∗G

erated by G is the set L(G) = {t ∈ TΣ | S ⇒ t}.
G

5.3

Known Results for LM-CFTG

First, we introduce normal forms for LM-CFTG. The reason fan-out rules andcontext-free rules are sufficient to define an LM-CFTG is based on Theorem 1.
Theorem 1. (Fujiyoshi [14]) [Chomsky-like normal form] Any LM-CFTG canbe transformed into an equivalent one whose rules are in one of the following
forms:(1) A → B(C) with A, C ∈ N0 and B ∈ N1 ,(2) A → a with A ∈ N0 and a ∈ Σ0 ,(3) A(x) → B(C(x)) with A, B, C ∈ N1 , or(4) A(x) → b(C1 , . . . , Ci−1 , x, Ci+1 , . . . , Cn ) with A ∈ N1 , n ≥ 1, b ∈ Σn , 1 ≤i ≤ n and C1 , . . . , Ci−1 , Ci+1 , . . . , Cn ∈ N0 .
See Fig. 9.
Theorem 2. (Fujiyoshi [14]) [Greibach-like normal form] Any LM-CFTG canbe transformed into an equivalent one whose rules are in one of the following
forms:

Verification of Mathematical Formulae Based on Formal Grammar
b

C1
a

A

Ci −1

A

B1

11

b

Ci +1

Cn

C1

Ci −1

A

B2

B1

Ci +1

Cn

B2

x

(1)
Bm

Bm

D

x

(2)

(3)

Fig. 10. Greibach-like normal form

(1) A → a with A ∈ N0 and a ∈ Σ0 ,(2) A → b(C1 , . . . , Ci−1 , u, Ci+1 , . . . , Cn ) with A ∈ N0 , n ≥ 1, b ∈ Σn , 1 ≤ i ≤ n,
C1 , . . . , Ci−1 , Ci+1 , . . . , Cn ∈ N0 and u ∈ TN , or
(3) A(x) → b(C1 , . . . , Ci−1 , u, Ci+1 , . . . , Cn ) with A ∈ N1 , n ≥ 1, b ∈ Σn , 1 ≤i ≤ n, C1 , . . . , Ci−1 , Ci+1 , . . . , Cn ∈ N0 , and u ∈ TN1 (x).
See Fig. 10. Since N is monadic, all trees in TN and TN1 (x) may be written
as B1 (B2 (· · · (Bm (D)) · · · )) and B1 (B2 (· · · (Bm (x)) · · · )), respectively, for somem ≥ 0, B1 , B2 , . . . , Bm ∈ N1 and D ∈ N0 . Note that m may be 0.
LM-CFTG is related to the tree adjoining grammar (TAG) [15–17], one of
the most famous and well-studied mildly context-sensitive grammar formalisms.
The definition of “weakly equivalent” is found in [3].
Theorem 3. (Fujiyoshi & Kasai [3]) LM-CFTG is weakly equivalent to TAG.
There exists an effective recognition algorithm for LM-CFTG.
Theorem 4. (Fujiyoshi [8]) There exists a recognition algorithm for LM-CFTG
that runs in O(n4 ) time, where n is the number of nodes of an input tree.
It is known that a recognition algorithm that runs in O(n3 ) time can beobtained with some modifications to the O(n4 )-time algorithm in [8].

6Conclusion and Future Work

We have proposed a verification method of mathematical formulae for a practicalmathematical OCR system based on a combination of context-free grammar andtree grammar. Though we have recognized the usefulness of the proposed verification method by experimental results, we know the necessity of the improvement

12

A. Fujiyoshi, M. Suzuki and S. Uchidaof the grammar defining “well-formed” mathematical formulae. Moreover, in order to avoid the ambiguity of the grammar, the inclusion of semantic analysis
needs to be considered.
In the future, we plan to internalize a verification system within the recognition engine of a mathematical OCR system. Because the flexibility of the grammar is important, we want to allow users to manipulate the grammar. Therefore,
we will reflect on ways users can update the grammar by themselves.

References
1. Chan, K.F., Yeung, D.Y.: Mathematical expression recognition: a survey. Int. J.
Document Analysis and Recoginition 3(1) (2000) 3–15
2. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages andComputation. Addison Wesley, Reading, Massachusetts (1979)
3. Fujiyoshi, A., Kasai, T.: Spinal-formed context-free tree grammars. Theory ofComputing Systems 33(1) (2000) 59–83
4. Anderson, R.: Syntax-directed recognition of hand-printed two-dimensional mathematics. In: Interactive Systems for Experimental Applied Mathematics. Academic
Press (1968) 436–459
5. Chou, P.A.: Recognition of equations using a two-dimensional stochastic contextfree grammar. In: Proc. SPIE. Volume 1199. (1989) 852–863
6. Kanahori, T., Sexton, A., Sorge, V., Suzuki, M.: Capturing abstract matrices
from paper. In: Proceedings of the 5th International Conference on Mathematical
Knowledge Management (MKM 2006), LNCS 4108 (2006) 124–138
7. Suzuki, M., Uchida, S., Nomura, A.: A ground-truthed mathematical characterand symbol image database. In: Proceedings of the 8th International Conference
on Document Analysis and Recognition (ICDAR 2005). Volume 2. (2005) 675–679
8. Fujiyoshi, A.: Application of the CKY algorithm to recognition of tree structures
for linear, monadic context-free tree grammars. IEICE Trans. Inf. & Syst. E90D(2) (2007) 388–394
9. Sikkel, K., Nijholt, A.: Parsing of Contex-Free Languages. In: Handbook of Formal
Languages. Volume 2. Springer-Verlag, Berlin (1997) 61–100
10. Suzuki, M., Tamari, F., Fukuda, R., Uchida, S., Kanahori, T.: Infty - an integrated
OCR system for mathematical documents. In: Proceedings of ACM Symposium
on Document Engineering 2003. (2003) 95–104
11. Infty Project, http://www.inftyproject.org/en/
12. Donnelly, C., Stallman, R.: Bison: The yacc-compatible parser generator. Available
on: http://www.gnu.org/software/bison/manual/ (2006)
13. Mozilla Firefox, http://www.mozilla.com/firefox/
14. Fujiyoshi, A.: Analogical conception of chomsky normal form and greibach normal
form for linear, monadic context-free tree grammars. IEICE Trans. Inf. & Syst.
E89-D(12) (2006) 2933–2938
15. Joshi, A.K., Levy, L.S., Takahashi, M.: Tree adjunct grammars. J. Computer &System Sciences 10(1) (1975) 136–163
16. Joshi, A.K., Schabes, Y.: Tree-adjoining grammars. In: Handbook of Formal
Languages. Volume 3. Springer-Verlag, Berlin (1997) 69–124
17. Abeillé, A., Rambow, O., eds.: Tree adjoining grammars: formalisms, linguistic
analysis and processing. CSLI Publications, Stanford, California (2000)

Verification of Mathematical Formulae Based on Formal Grammar

Appendix: Representative Sample of the Grammar
Defining “Well-Formed” Mathematical Formulae
Fan-Out Rules:

Exp
Int

Exp

∫

Int

∫
Exp

Exp

Σ

Sum

Σ

Sum

Exp

Exp

∏

Prod

∏

Prod

Lim

Σ

Sum

Range

∏

∏

Prod

Range

Init

lim

Σ
Range

Init

Init

Lim

Range

Range

Init

Prod

∫

Int

Exp

Exp
Sum

∫

Int

Range

Log

lim

log

Range

Range

Subscript

Supscript

Supscript
LetterNumericaLetter1b

LetterSubscript

Subscript

Exp

Exp

c

Sqrt

Frac
Exp

Exp

13

14

A. Fujiyoshi, M. Suzuki and S. UchidaContext-Free Rules:
M ath→ ExpList→ Sign ExpList

ExpList → Exp→ ExpList Sign Exp

Exp→ T erm→ U naryOp T erm

T erm

Range

→ Exp
→ Exp Sign Exp→ Exp Sign F actor Sign Exp

Init→ Exp ‘=’ Exp→ F actor→ T erm F actor→ T erm BinaryOp F actor→ ‘∞’

SubScript→ Exp→ Sign→ SubScript ‘,’ Exp→ SubScript ‘,’ Sign
→ Exp ‘=’ Exp

SupScript→ Exp→ Sign→ ‘0’ //prime→ ‘00’ //doubleprime→ ‘000’ //tripleprime

Sign

U naryOp → ‘+’
→ ‘−’
→ ‘±’
→ ‘∓’
→ ‘∀’
→ ‘∃’

→ ‘=’
→ ‘6=’
→ ‘<’
→ ‘≤’
→ ‘>’
→ ‘≥’
→ ‘∈’
→ ‘3’
→ ‘63’→ ‘⊂’→ ‘6⊂’→ ‘⊃’→ ‘6⊃’
→ ‘≡’
→ ‘∼
=’
→ ‘∼’
→ ‘→’
→ ‘⇒’
→ ‘↔’
→ ‘⇔’
→ ‘7→’→ ‘,’ //comma→ ‘;’ //semicolon→ ‘|’ //vert

BinaryOp→ ‘+’
→ ‘−’
→ ‘×’
→ ‘/’
→ ‘∩’
→ ‘∪’
→ ‘·’
→ ‘•’
→ ‘:’ //colon

Verification of Mathematical Formulae Based on Formal Grammar→ V ariable→ N umber
→∅
→∗
→4
→∇
→ℵ
→ ‘(’ ExpList ‘)’→ ‘[’ ExpList ‘]’→ ‘{’ ExpList ‘}’→ ‘(’ ExpList ‘]’→ ‘[’ ExpList ‘)’→ ‘h’ ExpList ‘i’→ F rac→ Sqrt→ ‘|’ Term ‘|’→ T rigOp F actor→ SumOp F actor→ F uncOp F actor

V ariable → Letter

T rigOp

→ Sin
→ Cos
→ T an

Sin
Cos
T an

SumOp

→ Int
→ Sum
→ P rod→ Bigcap→ Bigcup

Int
Sum
P rod
BigcapBigcup→ ‘sin’→ ‘cos’→ ‘tan’R→ ‘P’→ ‘Q ’→ ‘T ’→ ‘ S’
→‘ ’

Lim
Log
M in
M ax

→ ‘lim’→ ‘log’→ ‘min’→ ‘max’F actorF uncOp → Lim→ Log→ M in→ M axLetter

→ ‘a’
→ ‘b’
..
.
→ ‘z’

N umber → Integer→ Integer ‘.’ Integer→ ‘.’ Integer
Integer→ N umeric→ Integer N umeric

N umeric → ‘0’
→ ‘1’
..
.
→ ‘9’

15