Skip to main content
PRL Project

A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

  • unofficial copies PDF, PS
  • Cornell Tech Report
  • International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, Vol 3119, pp. 220-235, 2004.

As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. We apply graph-based approaches, such as HITS, or Hyperlink-Induced Topic Search, [11] used for World Wide Web document search and analysis, to formal mathematical data collections. The nodes of the graphs we analyze are theorems and definitions, and the links are logical dependencies. By exploiting this link structure, we show how one may extract organizational and relatedness information from a collection of digital formal math. We discuss the value of the information we can extract, yielding potential applications in math search tools, theorem proving, and education.

bibTex ref: CEKL04

cite link