A proof-theoretic approach to mathematical knowledge management

摘要: Mathematics is an area of research that forever growing. Definitions, theorems, axioms, and proofs are integral part every mathematics. The relationships between these elements bring to light the elegant abstractions bind even most intricate aspects math science. As body mathematics becomes larger its become richer, organization mathematical knowledge more important difficult. This emerging referred as management (MKM). primary issues facing MKM were summarized by Buchberger, one organizers first Mathematical Knowledge Management Workshop [20]. (1) How do we retrieve from existing future sources? (2) How build bases? (3) How make bases available mathematicians? These questions have particularly relevant with growing power interest in automated theorem proving, using computer programs prove theorems. Automated provers been used formalize theorems all areas mathematics, resulting large libraries knowledge. However; usually implemented at system level, meaning they not defined same level formalism themselves, which rely on a strong underlying proof theory rules for their creation. In this thesis, develop proof-theoretic approach formalizing library way steps formalized provers. formal exhibits five desirable properties: independence, structure, formalism, adaptability, presentability. ultimate goal vast information people skill levels. thesis provides foundation realizing goal.