index.md

---
layout: page
title: KWARC Research
menu_title: Overview
hidden: true
---
 The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management.
 We extend techniques from [formal methods](formal-methods/) so that they can be used in settings where formalization is either infeasible or too costly.
 We concentrate on developing techniques for marking up the [structural semantics](structural-semantics/) in technical documents.
 This level of markup allows for offering interesting [knowledge management services](kminteract/) without forcing the author to fully formalize the document contents, we are working on methods for [semi-automated semantization](semantization/).
 All in all, the research in the KWARC group is summarized in the schema below, which can be read as a pipeline from foundations (on the bottom) to applications (on the top).


<table style="border: 1px solid black">
  <col width="33%"/>
  <col width="33%"/>
  <col width="33%"/>
  <tbody>
    <tr style="border: 1px solid black">
      <td colspan="3">
    <span style="font-weight:bold">Applications</span>
    eMath 3.0,
    <a href="https://mathhub.info">Active Documents</a>,
    <a href="/projects/SiSsI/">Semantic Spreadsheets</a>,
    <a href="/projects/FormalCAD/">Semantic CAD/CAM</a>,
    Semantic Help Systems, Change Mangagement, ...
      </td>
    </tr>
    <tr>
      <td style="border: 1px solid black">
    <span style="font-weight:bold">Foundations of Mathematics</span>
    <ul>
      <li><a href="https://omdoc.org">OMDoc</a></li>
      <li><a href="http://uniformal.github.io">MMT: Modular Math Theories</a></li>
      <li><a href="/projects/latin">Logic Morphisms/Atlas</a></li>
      <li>Advanced Type Theories</li>
      <li><a href="/projects/oaf/">Theorem Prover</a> and <a href="../projects/odk/">Computer Algebra</a>  Interoperability</li>
    </ul>
      </td>
      <td style="border: 1px solid black">
    <a href="research/kminteract"><span style="font-weight:bold">Knowledge Mgt. &amp; Interaction</span></a>
    <ul>
      <li>Semantic Interpretation</li>
      <li><a href="https://github.com/KWARC/jobad">JOBAD: Document-Embedded Interaction</a></li>
      <li><a href="/systems/mws/">Math Web Search</a></li>
      <li>Math Archives</li>
    </ul>
      </td>
      <td style="border: 1px solid black">
    <a href="research/semantization">
      <span style="font-weight:bold">Semantization</span>
    </a>
    <ul>
      <li><a href="/systems/arXMLiv/">LaTeX --&gt; XML</a></li>
      <li><a href="/systems/sTeX/">sTeX: Semantic LaTeX</a></li>
      <li>Invasive editors</li>
      <li>Context-Aware IDEs</li>
      <li>Mathematical Corpora</li>
      <li><a href="/systems/llamapun/">Linguistics of Math</a></li>
    </ul>
      </td>
    </tr>
    <tr style="border: 1px solid black">
      <td colspan="3">
    <span style="font-weight:bold">Foundations:</span>
    Computational Logic,
    <a href="formal-methods/">Formal Methods</a>,
    <a href="http://www.w3.org/TR/MathML3/">MathML</a>,
    <a href="http://openmath.org">OpenMath</a>
      </td>
    </tr>
  </tbody>
</table>

The KWARC Group welcomes student involvement in research. If you are interested, please send an e-mail to <michael.kohlhase@fau.de>, or come to our seminars and courses

We have an initial list topics for [theses, or guided research](https://gl.kwarc.info/kwarc/thesis-projects)