A Proof-Theoretic Approach to Mathematical Knowledge Management

dc.contributor.authorAboul-Hosn, Kamal
dc.description.abstractMathematics 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.en_US
dc.format.extent2044039 bytes
dc.relation.isformatofbibid: 6476235
dc.subjectproof theoryen_US
dc.subjectmathematical knowledge managementen_US
dc.subjecttheorem proversen_US
dc.titleA Proof-Theoretic Approach to Mathematical Knowledge Managementen_US
dc.typedissertation or thesisen_US


Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
1.95 MB
Adobe Portable Document Format