Conferences on Intelligent Computer Mathematics - Birmingham 2008
CICM '08

Doctoral Programme

Birmingham, UK, 29-31 July 2008

Christoph Lange: Web Collaboration on Semiformal Mathematical Knowledge

The overall goal of my Ph.D. research (started in September 2006, expected graduation in August 2009) is to investigate the foundations of web collaboration on structured, semiformal mathematical knowledge, to practically implement the theoretical model developed, and to use the resulting system in relevant case studies in order to validate the assumptions made. Leitmotiv of the conceptual and technical design of the system is: How can users be motivated and supported to make the effort of structuring mathematical knowledge, what additional knowledge can be inferred from users' contributions, and how can this again be utilised in order to improve collaboration? This is motivated by the lack of knowledge management services in existing collaborative platforms for mathematics. As a concrete technical basis I have chosen to integrate the OpenMath and OMDoc semantic markup languages into a semantic wiki, i.e. a wiki using semantic web technologies like RDF and ontologies, that allows for reading, browsing, editing, and restructuring mathematical knowledge items. The work done so far has focused on engineering a semantic web ontology of types of mathematical statements and their interrelations. This ontology serves as the vocabulary of an RDF knowledge graph extracted from document markup, which is then subject to reasoning that enables browsing/editing/searching services. Representing notations of symbols and the connection between structures of mathematical knowledge and user interaction, such as discussions about formalisation issues, were use cases of particular concern. One case study, the deployment phase of which will start in summer 2008, deals with editing OpenMath content dictionaries in the context of the preparation of OpenMath 3 and focuses on notations and metadata. Results will then be transferred to the more formal and more complex OMDoc. The other case study, for which the requirements have been analysed and some services been developed so far, will deal with text annotation, stepwise formalisation, discussion, project management, and documentation in the context of the large-scale proof formalisation effort Flyspeck. My current focus, visiting the semantic web research institute DERI for half a year, is on extending the above-mentioned ontology for mathematical statements and integrating it with an ontology that models narrative and rhetorical structures of scientific documents, aiming at a better support for the range between unstructured text and formal mathematical knowledge and facilitating reuse of semi-formal knowledge items in linearly ordered documents