A Proof-Theoretic Approach to Mathematical Knowledge Management

Other Titles

Mathematics is an area of research that is forever growing. Definitions, theorems, axioms, and proofs are integral part of every area of mathematics. The relationships between these elements bring to light the elegant abstractions that bind even the most intricate aspects of math and science.

As the body of mathematics becomes larger and its relationships become richer, the organization of mathematical knowledge becomes more important and more difficult. This emerging area of research is referred to as mathematical knowledge management (MKM). The primary issues facing MKM were summarized by Buchberger, one of the organizers of the first Mathematical Knowledge Management Workshop.

-How do we retrieve mathematical knowledge from existing and future sources? -How do we build future mathematical knowledge bases? -How do we make the mathematical knowledge bases available to mathematicians?

These questions have become particularly relevant with the growing power of and interest in automated theorem proving, using computer programs to prove mathematical theorems. Automated theorem provers have been used to formalize theorems and proofs from all areas of mathematics, resulting in large libraries of mathematical knowledge. However, these libraries are usually implemented at the system level, meaning they are not defined with the same level of formalism as the proofs themselves, which rely on a strong underlying proof theory with rules for their creation.

In this thesis, we develop a proof-theoretic approach to formalizing the relationships between proofs in a library in the same way the steps of a proof are formalized in automated theorem provers. The library defined in this formal way exhibits five desirable properties: independence, structure, an underlying formalism, adaptability, and presentability. The ultimate goal of mathematical knowledge management is to make the vast libraries of mathematical information available to people at all skill levels. The proof-theoretic approach in this thesis provides a strong formal foundation for realizing that goal.

Journal / Series
Volume & Issue
Date Issued
proof theory; mathematical knowledge management; theorem provers
Effective Date
Expiration Date
Union Local
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
bibid: 6476235
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
Link(s) to Reference(s)
Previously Published As
Government Document
Other Identifiers
Rights URI
dissertation or thesis
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record