ÿþTheorema and Mathematical Knowledge Management



Bruno Buchberger



IMA 2002 Summer Program: Special Functions in the Digital Age, July 22 - August 2, 

2002, University of Minnesota, Minneapolis, USA.





ABSTRACT:



Mathematical Knowledge Management (MKM) is a new area that aims at computer-supporting

the access, over the web, to mathematical knowledge. MKM has various layers of 

sophistication:



- accessing mathematical knowledge in the form of texts generated within systems like

TeX, MathMl etc. that allow to represent formulae in the usual mathematical notation



- semantic annotation of files containing mathematical text (the "semantic web")



- accessing and processing mathematical knowledge as formulae in a well-defined logic 

language like predicate logic.



In the talk we are concerned with MKM in the frame of predicate logic. Processing

mathematical knowledge in this context needs automated theorem proving and other 

formal tools and will drastically change the way how mathematics is done in the 

future. 



We describe the Theorema system and discuss its current and future tools for MKM.