Narrative structure of mathematical texts
Proceedings of the Sixth International Conference on MATHEMATICAL KNOWLEDGE MANAGEMENT, Lecture Notes in AI 4573, page 296-312. Springer, (2007)Abstract
There are many styles for the narrative structure of a mathe-
matical document. Each mathematician has its own conventions and tra-
ditions about labeling portions of texts (e.g., chapter, section, theorem or
proof ) and identifying statements according to their logical importance
(e.g., theorem is more important than lemma). Such narrative/struc-
turing labels guide the reader’s navigation of the text and form the key
components in the reasoning structure of the theory reflected in the text.
We present in this paper a method to computerise the narrative structure
of a text which includes the relationships between labeled text entities.
These labels and relations are input by the user on top of their natural
language text. This narrative structure is then automatically analysed
to check its consistency. This automatic analysis consists of two phases:
(1) checking the good-usage of labels and relations (i.e., that a “proof”
justifies a “theorem” but cannot justify an “axiom”) and (2) checking
that the logical precedences in the document are self-consistent.
The development of this method was driven by the experience of com-
puterising a number of mathematical documents (covering different au-
thoring styles). We illustrate how such computerised narrative structure
could be used for further manipulations, i.e. to build a skeleton of a
formal document in a formal system like Mizar, Coq or Isabelle.
