Guided Research

Below are some of the topics offered by the KWARC group. Always contact Prof. Kohlhase for both custom-fitted and below listed topics.

Logics and Formal Documents

For a list of further topics in the general area of logic, go to the homepage of the MMT project

Open Guided Research Topics in the panta rhei project!!!

Go to the panta rhei website and browse through our open topics!!!

Problem-Solving in Math Knowledge Bases by Argumentation

Full description (place your questions and comments there; you need to register for an account)
Note that this description includes material for more than one guided research project:

• evaluation
• implementing assistance
• corpus studies
• automated agents

History Visualization of Mathematical Documents

Full description (place your questions and comments there; you need to register for an account)

Interactive Math Notation Editor

Full description (place your questions and comments there; you need to register for an account)

Implement and evaluate editor extensions for annotating special structures of mathematical knowledge

Full description (place your questions and comments there; you need to register for an account)

Exporting mathematical document collections to PDF

Full description (place your questions and comments there; you need to register for an account)

Extracting Knowledge from Semantic Web and Web 2.0 Resources with Krextor

Full description (place your questions and comments there; you need to register for an account)

Providing context-sensitive editing help in the SWiM wiki

Full description (place your questions and comments there; you need to register for an account)

Study the applicability of OMDoc as a Semantic Web ontology language

Full description (place your questions and comments there; you need to register for an account)

Implement and evaluate a two-way conversion OMDoc↔XHTML+RDFa

Full description (place your questions and comments there; you need to register for an account)

Testing the integration of SWiM and MathWebSearch

Full description (place your questions and comments there; you need to register for an account)

Integrating SWiM and Mathematica

Full description (place your questions and comments there; you need to register for an account)

Generalization Queries for MathWebSearch

The MathWebSearch formula search engine currently only does instantiation queries, where formula metavariables in queries are instantiated. The implementation should be extended to handle queries, where universally quantified variables in the index are instantiated. An application of this is the search for appliccable results.

Transformation of the ACL2 library to OMDoc

The same idea as above, only here the syntax is in LISP. (remember: ACL2 Book is $15 from the website; also talk to Matt Kaufmann)

PVS to OMDoc transformation (XSL; ambitious)

PVS is a higher-order theorem prover wit a very substantial library. It can output XML system-near versions, so here we we only have to write an XSLT stylesheet here

Translate the Mizar library to OMDoc

Represent Gröthendieck set theory in OMDoc and implement a translation from Mizar theories preserving the import structure.

Implement and test the OpenMath binary encoding

The Openmath Standard specifies a binary encoding for OpenMath Objects. A parser and emitter for this should be implemented in Java and C.

Automated parser generation for OMDoc notation definitions

Identify a sublanguage of the presentation language for OpenMath objects for which presentations can be parsed back uniquely and implement the parser generation.

A Part-of-speech analyzer for mathematical texts

This does some linguistic analysis for legacy scientific texts