overview.md

---
layout: page
title: KWARC Research
menu_title: Overview
menu_order: 101
---
 The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management. We extend techniques from [formal methods](http://kwarc.info/research/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](http://kwarc.info/structural-semantics) in technical documents. This level of markup allows for offering interesting [knowledge management services](http://kwarc.info/research/kminteract/) without forcing the author to fully formalize the document contents, we are working on methods for [semi-automated semantization](http://kwarc.info/research/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>
  <tbody>
    <tr>
      <td colspan="3">
	<span style="font-weight:bold">Applications</span>
	eMath 3.0,
	<a href="https://planetary.mathweb.org">Active Documents</a>,
	<a href="https://trac.kwarc.info/sissi">Semantic Spreadsheets</a>,
	<a href="https://trac.kwarc.info/FormalCAD">Semantic CAD/CAM</a>,
	Semantic Help Systems, Change Mangagement, ...
      </td>
    </tr>
    <tr>
      <td>
	<span style="font-weight:bold">Foundations of Mathematics</span>
	<ul>
	  <li><a href="https://omdoc.org">OMDoc</a></li>
	  <li>advanced Type Theories</li>
	  <li><a href="http://uniformal.github.io">MMT: Modular Math Theories</a></li>
	  <li><a href="http://trac.omodoc.org/LATIN">Logic Morphisms/Atlas</a></li>
	  <li>Theorem Prover Interoperability</li>
	</ul>
      </td>
      <td>
	<a href="http://kwarc.info/research/kminteract"><span style="font-weight:bold">Knowledge Mgt. &amp; Interaction</span></a>
	<ul>
	  <li>Semantic Interpretation</li>
	  <li><a href="https://trac.omdoc.org/JOBAD">JOBAD: Document-Embedded Interaction</a></li>
	  <li><a href="https://trac.mathweb.org/tntbase">TNTBase: Versioned XML Storage</a></li>
	  <li><a href="http://trac.mathweb.org/MWS">Math Web Search</a></li>
	  <li>Math Archives</li>
	</ul>
      </td>
      <td>
	<a href="http://kwarc.info/research/semantization">
	  <span style="font-weight:bold">Semantization</span>
	</a>
	<ul>
	  <li><a href="http://github.com/brucemiller/LaTeXML">LaTeX --&gt; XML</a></li>
	  <li><a href="http://github.com/KWARC/sTeX">sTeX: Semantic LaTeX</a></li>
	  <li>invasive editors</li>
	  <li>Context-Aware IDEs</li>
	  <li>Mathematical Corpora</li>
	  <li><a href="https://github.com/KWARC/llamapun">Linguistics of Math</a></li>
	</ul>
      </td>
    </tr>
    <tr>
      <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>