A Proof-Theoretic Approach to Mathematical Knowledge Management
| dc.contributor.author | Aboul-Hosn, Kamal | |
| dc.date.accessioned | 2006-12-08T15:22:19Z | |
| dc.date.available | 2006-12-08T15:22:19Z | |
| dc.date.issued | 2006-12-08T15:22:19Z | |
| dc.description.abstract | 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. | en_US |
| dc.format.extent | 2044039 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.identifier.uri | https://hdl.handle.net/1813/3936 | |
| dc.language.iso | en_US | en_US |
| dc.relation.isformatof | bibid: 6476235 | |
| dc.subject | proof theory | en_US |
| dc.subject | mathematical knowledge management | en_US |
| dc.subject | theorem provers | en_US |
| dc.title | A Proof-Theoretic Approach to Mathematical Knowledge Management | en_US |
| dc.type | dissertation or thesis | en_US |
Files
Original bundle
1 - 1 of 1