systems/meta/index.md

+---
+layout: default
+title: Systems and Libraries
+permalink: /systems/
+---
+
+{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
+
+<ul class="collection">
+    {% for item in systems %}
+        {% unless item.end_date %}
+            {% include psitem.html item=item %}
+        {% endunless %}
+    {% endfor %}
+</ul>

systems/meta/orphans.md

+---
+layout: page
+title: Orphaned Systems up for Adoption
+permalink: /systems/orphans/
+---
+
+Many of the KWARC projects are the work of students and become orphaned when these move on
+to greener pastures (e.g. when they graduate). We put these systems up for adoption bt new
+students. If you are interested, please contact someone from the KWARC group, we would be
+happy to help you understand the development opportunities and get involved. 
+
+{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
+
+<ul class="collection">
+    {% for item in systems %}
+        {% if item.orphan %}
+            {% include psitem.html item=item %}
+        {% endif %}
+    {% endfor %}
+</ul>
\ No newline at end of file

systems/mmt.md

 ---
 layout: system
-menu_title: MMT
-title: "MMT: Meta Meta Theories/Meta Meta Tool"
+
+title: "MMT"
+shorttitle: MMT
 teaser: A framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.
-people: frabe,dmueller,twiesing,miancu,fhorozal
+
+start_date: 2011-03
+
+people: 
+    - frabe
+    - dmueller
+    - twiesing
+    - miancu
+    - fhorozal
+    - mkohlhase
+    - nroux
+
+supported-by:
+    - oaf
+    - odk
+    - latin
+    - mathsearch
+
+logo: public/mmt_logo.svg
+publink: http://kwarc.github.io/bibs/mmt
+website: https://uniformal.github.io/
+repository: https://github.com/Uniformal/MMT
 ---
 
 MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. It achieves a high level of generality by systematically avoiding a commitment to a particular syntax or semantics. Instead, individual language features (e.g., λ-abstraction, conjunction, etc.) and syntax features (keywords, notations, etc.) are defined as separate, reusable modules, from which individual languages are assembled. These modules can be declarative by specifying features as Mmt theories or programmatic by providing individual rules as plugins.Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level. These include knowledge management algorithms (e.g, IDE, search, change management) as well as logical algorithms (e.g., parsing, type reconstruction, module system). Thus, we can use MMT to obtain strong implementations of declarative languages at extremely low cost.Moreover, the focus on modularity and language-independence enables system integration, where MMT can mediate the exchange of knowledge across different foundational systems and concrete syntaxes.See here for the MMT homepage.

systems/mws.md

 ---
 layout: system
+
 menu_title: MathWebSearch
-title: "MathWebSearch a Mathematical Search Engine"
-pillar: KMR
-start: 2005
-people: mkohlhase,isucan,cprodescu,rhambasan,ahambasan
+shorttitle: MWS
+title: MathWebSearch
+teaser: A Mathematical Search Engine
+
+start_date: '2005'
+orphan: true
+people: 
+    - mkohlhase
+    - isucan
+    - cprodescu
+    - rhambasan
+    - ahambasan
+    - twiesing
+supported-by:
+    - mathsearch
+    - odk
+    - oaf
+
+<!-- logo: public/kwarc_logo.svg -->
+website: http://search.mathweb.org
+repository: https://github.com/MathWebSearch
+publink: http://kwarc.github.io/bibs/mws
 ---
 
 The MathWebSearch system (MWS) is a content-based search engine for mathematical
 formulae. It indexes MathML formulae, using a technique derived from automated theorem
-proving: Substitution Tree Indexing. Find more information at the
-[Project Overview Page](http://search.mathweb.org) or the
-[GitHub Repository](http://githhub.com/KWARC/mws).
+proving: Substitution Tree Indexing. With this indexing technique MWS can answer
+unification queries extremely efficiently (30-100 ms) on large sets of formulae (in the
+Gigaformula range); but the index (up to 50GiB) needs to be kept in main memory.
+
+MWS is the [formula search engine](https://zbmath.org/formulae/) employed in
+[Zentralblatt Math](http://zbmath.org); see a
+[demo on a mathematical subset](http://arxivsearch.mathweb.org) of the
+[arXMLiv data set](/projects/arXMLiv/) [further demos](http://search.mathweb.org).
+
+The MathWebSearch system is Open Source,
+[developed on GitHub](https://github.com/MathWebSearch), and is (by now) easily deployable via
+a set of docker containers. We can give your project a search interface like the
+[nLab search](https://nlabsearch.mathweb.org/) for [nLab](https://ncatlab.org/) at the
+cost of theming the [user interface](https://github.com/MathWebSearch/frontend) and
+[building a harvester](https://github.com/MathWebSearch/nlab_harvester).

systems/omdoc.md

 ---
 layout: system
-menu_title: OMDoc
+
 title: "OMDoc: Open Mathematical Documents"
-teaser: A markup format and data model for Open Mathematical Documents. It serves as semantics-oriented representation format and ontology language for mathematical knowledge.
-homepage: http://omdoc.org
-repository: http://github.com/OMDoc
-people: mkohlhase
+shorttitle: OMDoc
+teaser: A markup format and data model for Open Mathematical Documents and Knowledge
+
+start_date: '1998'
+
+people: 
+    - mkohlhase
+    - miancu
+    -  nmueller
+    - frabe
+
+supported-by:
+    - Jem
+    - mathsearch
+    - omoc
+    - openmath-tn
+    - logosphere
+    - once-cs
+
+logo: public/omdoc_logo.png
+website: http://omdoc.org
+repository: https://github.com/OMDoc
+publink: http://kwarc.github.io/bibs/omdoc
 ---
 
-OMDoc is a markup format and data model for Open Mathematical Documents. It serves as semantics-oriented representation format and ontology language for mathematical knowledge.
+OMDoc is a markup format and data model for Open Mathematical Documents. It serves as
+semantics-oriented representation format and ontology language for mathematical
+knowledge. The formal part of OMDoc has been refined into the
+[MMT format](https://uniformal.github.com), and we use the
+[MMT System](https://uniformal.github.com) as the reference implementation.
+
+We are currently working on extending MMT to cover the full flexiformal coverage of
+OMDoc. 

systems/openmathmap.md

 ---
 layout: system
-menu_title: OpenMathMap
+
 title: OpenMathMap
+shorttitle: OpenMathMap
 teaser: A Map of Mathematics
-start: 2013-06
+
+start_date: 2013-06 
+end_date: 2015-06 
+orphan: true
+
+people:
+    - mkohlhase
+
+supported-by:
+    - mathsearch
+logo: public/kwarc_logo.svg
+website: http://map.mathweb.org
 repository: https://github.com/KWARC/openmathmap/
-homepage: http://map.mathweb.org
-people: mkohlhase
 ---
-OpenMathMap project, a recognizable, interactive map of mathematical areas from the MSC an Zentralblatt Publication Data.
+OpenMathMap project, a recognizable, interactive map of mathematical areas from the MSC an
+Zentralblatt Publication Data. A demo is (sometimes) running on http://map.mathweb.org

systems/sTeX.md

 ---
 layout: system
-menu_title: sTeX
+
 title: "sTeX: Semantic Markup for LaTeX"
-pillar: semantization
-start: 2004-09
-people: mkohlhase,dginev
+shorttitle: sTeX
+
+start_date: 2004-09
+
+people: 
+    - mkohlhase
+    - dginev
+    - twiesing
+collaborators:
+    - Dr. Bruce Miller (NIST)	
+
+supported-by:
+    - sissi
+    - mathsearch
+    - odk
+
+logo: public/kwarc_logo.svg
+repository: https://github.com/KWARC/sTeX
+publink: http://kwarc.github.io/bibs/sTeX
 ---
+
 The TeX/LaTeX workflow is deeply embedded into mathematical practice. Therefore the sTeX
-system allows to embed [/structural semantics](/research/structural-semantics) into documents. For details see the [sTeX project on GitHub](https://github.com/KWARC/sTeX).
+system allows to embed [/structural semantics](/research/structural-semantics) into
+documents. Concretely sTeX is a "semantic version of LaTeX" that allows to use special
+macros to encode mathematical meaning explicitly. This is (largely ignored in PDF
+generation), but can be taken into account when generating [OMDoc-based](/systems/omdoc/) active documents.
+
+## Resources
+* [sTeX at GitHub](https://github.com/KWARC/sTeX) and the corresponding
+[LaTeXML](http://dlmf.nist.gov/LaTeXML/)
+[plugin for sTeX](https://github.com/KWARC/LaTeXML-Plugin-sTeX)
+* Some sTeX-based libraries of active doucents on [MathHub.info](http://mathhub.info): [SMGloM](https://mathhub.info/smglom), [active course notes](https://mathhub.info/MiKoMH).  
+* Their sources can be found here: [SMGloM](https://gl.mathhub.info/smglom), [active course notes](https://gl.mathhub.info/MiKoMH).  
 
+## Documentation/Papers
+* M. Kohlhase (2008) [*Using LaTeX as a semantic markup format*](https://kwarc.info/kohlhase/papers/mcs08-stex.pdf). Mathematics in Computer Science 2 (2), pp. 279–304
+* ... [complete bibliography](http://kwarc.github.io/bibs/sTeX)

systems/sally.md

 ---
 layout: system
-menu_title: Semantic Alliance
+
 title: Semantic Alliance
+shorttitle: Sally
 teaser: A framework for mashing up semantic services into desktop applications.
+
+start_date: 2013-02
+start_date: 2016-08
+orphan: true
+
+people: 
+    - mkohlhase
+    - akohlhase
+    - cjucovschi
+
+supported-by:
+    - sissi
+    - FormalCAD
+
+logo: public/kwarc_logo.svg
 repository: https://github.com/KWARC/Sally
-people: mkohlhase,akohlhase,cjucovschi
+publink: http://kwarc.github.io/bibs/sally
 ---
+A distributed framework for mashing up semantic services into desktop applications.
+

systems/smglom.md

 ---
 layout: system
-menu_title: SMGloM
-title: "The Semantic, Multilingual Glossary of Mathematics"
-pillar: KMR
-start: 2013-11
-people: mkohlhase,cjucovshi,miancu
+
+title: "SMGLoM - A Semantic, Multilingual Glossary of Mathematics"
+shorttitle: SMGLoM
+teaser: A terminological resource for Mathematics
+start_date: 2013-11
+
+people: 
+    - mkohlhase
+    - cjucovschi
+    - miancu
+    - twiesing
+    - jfschaefer
+
+supported-by:
+    - mathsearch
+    - odk
+logo: public/kwarc_logo.svg
+publink: https://kwarc.github.io/bibs/smglom
 ---
-The [Semantic, Multilingual Glossary of Mathematics](/systems/smglom/) is a 
+The SMGloM is a structured terminology for mathematics. It combines lexical information about the "Words of Mathematics" (in multiple languages) with semantic information about their dependencies. Multiple services can be derived from this terminology, e.g. a [classical glossary](https://mathhub.info/applications/glossary) and a [math dictionary](https://mathhub.info/applications/dictionary).
+
+## Resources
+* [SMGloM at MathHub.info](https://mathhub.info/library/group?id=smglom)
+* [the SMGloM sources on gl.mathhub.info](https://gl.mathhub.info/smglom),
+  written in [sTeX](/systems/sTeX) (a semantic version of LaTeX)
+* a [generated dictionary](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/dictionary.en-de-ro-zhs.pdf)
+* various generated glossaries on the 
+  [SMGloM applications repository](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/) for
+  [English](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.en.pdf),
+  [German](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.de.pdf),
+  [Chinese (simplified)](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.zhs.pdf),
+  [Romanian](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.ro.pdf)
+
+## Papers
+* D. Ginev, M. Iancu, C. Jucovshi, A. Kohlhase, M. Kohlhase, A. Oripov, J. Schefter, W. Sperber, O. Teschke and T. Wiesing (2016) [The SMGloM project and system: towards a terminology and ontology for mathematics](https://kwarc.info/kohlhase/papers/icms16-smglom.pdf) ICMS 2016
+* M. Kohlhase (2014) [A data model and encoding for a semantic, multilingual terminology of mathematics](https://kwarc.info/kohlhase/papers/cicm14-smglom.pdf) CICM 2014
+* [complete bibliography](https://kwarc.github.io/bibs/smglom/)
+* [blue notes](https://gl.kwarc.info/smglom/blue): epsilon-baked ideas about how to continue

systems/swim.md

 ---
 layout: system
-menu_title: SWIM
+
 title: "SWiM: Semantic Wiki for Mathematics"
-start: 2006-08
-end: 2009-06
-people: mkohlhase,clange
+shorttitle: SWiM
+teaser: A Semantic Wiki for Interactive Mathematics.
+
+start_date: 2006-08
+end_date: 2009-06
+publink: http://kwarc.github.io/bibs/swim
+logo: public/kwarc_logo.svg
+
+people: 
+    - clange
+    - mkohlhase 
 ---
+
 SWIM is a Semantic Wiki for Interactive Mathematics. The system has been superseded by [MathHub](/systems/mathhub/).

systems/tgview3d.md

+---
+layout: system
+
+menu_title: TGView3D
+shorttitle: TGView3D
+title: The TGView3D Graph Viewer
+teaser: An interactive 3D graph viewer optimized for visualizing Theory Graphs and mathematical knowledge in general
+
+start_date: '2018'
+
+people: 
+    - mkohlhase
+    - frabe
+    - dmueller
+    - rmarcus
+
+
+supported-by:
+    - odk
+
+website: https://tgview3d.mathhub.info/
+repository: https://github.com/UniFormal/tgview3d
+publink: https://kwarc.info/people/mkohlhase/submit/cicm20-tgview3D.pdf
+---
+The TGView3D System is a 3D-theory graph viewer in the Unity Engine.
+Different layouts and highlighting settings are available to visualize the complex theory graphs efficiently.
+In particular, this allows exploration of big mathematical libraries, e.g, those related to theorem provers like Coq or Isabelle.
+Furthermore, we have a virtual reality protoype to allow intuitive and immersive interactions.
+
+
+*For students*: Topics for theses and projects are available [here](https://gl.kwarc.info/kwarc/thesis-projects/-/issues?label_name%5B%5D=Graph+Visualization).
\ No newline at end of file

teaching/AIProj.md

----
-layout: course
-instructor: mkohlhase
-title: Projekt zur Künstlichen Intelligenz
-menu_title: KI-Projekt
-taught: WS16/17, SS16
----
-
-The KWARC group (Wissensrepräsentation und Verarbeitung)conducts research in knowledge representation and reasoning techniques with a view towards applications in knowledge management. 
-We extend techniques from 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 in technical documents. 
-This level of markup allows for offering interesting knowledge management services without forcing theauthor to formalize the document contents. 
-In contrast to courses with fixed topics, project topics are defined individually.
-
-See the [KWARC home page](http://kwarc.info) for a general introduction to the research and [the KWARC research topics list](http://gl.kwarc.info/kwarc/thesis-projects) for expemplary topics. 

teaching/KRMT.md

----
-layout: course
-instructor: mkohlhase
-title: Vorlesung *Logik-Basierte Wissensrepräsentation für Mathematisch/Technisches Wissen*
-menu_title: Vorlesung KRMT
-taught: SS16/17
----
-
-Dieser Kurs behandelt Grundlagen der Mathematik, Modulare Formalisierung in
-Theoriegraphen, Narrative Strukturen in informellen mathematisch/technischen Dokumenten,
-Formalisierung von Logiksprachen in Metalogiken.
-
-Da wir nur wenige Studenten erwarten, wollen wir diesen Kurs sehr interaktiv und
-Projektorientiert aufbauen. 
-

teaching/ai1.md

----
-layout: course
-instructor: mkohlhase
-title: Künstliche Intelligenz I
-menu_title: Künstliche Intelligenz I
-taught: WS16
----
-Diese Vorlesung beschäftigt sich mit den Grundlagen der Künstlichen Intelligenz (KI), insbesondere formale Wissensrepräsentation, Heuristische Suche, Automatisches Planen und Schliessen unter Unsicherheit.
-

teaching/ai2.md

----
-layout: course
-instructor: mkohlhase
-title: Künstliche Intelligenz II
-menu_title: Künstliche Intelligenz II
-taught: SS16/17
----
-
-Dieser Kurs beschäftigt sich mit den Grundlagen der Künstlichen Intelligenz (KI), insbesondere mit Techniken des Schliessens unter Unsicherheit, des maschinellen Lernens und dem Sprachverstehen.
-Der Kurs baut auf der Vorlesung Künstliche Intelligenz I vom Wintersemester auf und führt diese weiter.
-

teaching/wuv.md

----
-layout: course
-instructor: mkohlhase
-title: Seminar Wissensrepräsentation und -verarbeitung
-menu_title: Seminar WuV
----
-
-This seminar covers topics from knowledge representation and knowledge processing, mostly
-with a focus on mathematical knowledge.
-