Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. A Graph-Based Approach towards Discerning Inherent Structures in a
    Digital Library of Formal Mathematics

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

File(s)
TR2006-2015.pdf (185.78 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5715
Collections
Computing and Information Science Technical Reports
Author
Lorigo, Lori
Kleinberg, Jon
Eaton, Richard
Constable, Robert
Abstract

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.

Date Issued
2006-01-30
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2006-2015
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance