research/structural-semantics.md

@@ -4,8 +4,8 @@ title: Structural Semantics
 menu_order: 103
 ---
 
-Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with [formal methods](formal-methods/).
-In many cases, useful [mathematical services](kminteract/) can be rendered by machines without having an [entailment relation](formal-methos/), for instance we can search for a formula, we can determine the concepts it depends upon, etc.
+Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with [formal methods](../formal-methods/).
+In many cases, useful [mathematical services](../kminteract/) can be rendered by machines without having an [entailment relation](../formal-methods/), for instance we can search for a formula, we can determine the concepts it depends upon, etc.
 The commonality of such services is that they are based on the structure of the formulae alone.
 For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
 We speak of *structural semantics* as a lightweight form of meaning annotation. 

systems/frameit.md

+---
+layout: system
+
+menu_title: FrameIt
+shorttitle: FrameIT
+title: The UFrameIT Framework
+teaser: A Framework for Serious Games by combining Virtual Worlds with Mathematical Knowledge Management
+
+start_date: '2013'
+
+people: 
+    - mkohlhase
+    - dmueller
+    - rmarcus
+    - nroux
+    - jschihada
+
+supported-by:
+    - oaf
+
+website: https://uframeit.org
+repository: https://github.com/UFrameIT
+publink: http://kwarc.github.io/bibs/frameit
+---
+
+The FrameIT project builds a Framework for Serious Games by combining Virtual Worlds with
+Mathematical Knowledge Management. The main idea is that we can use 
+[MMT](https://kwarc.info/projects/mmt) theory graphs to represent the background knowledge
+and [MMT](https://kwarc.info/projects/mmt) pushouts to compute the application of
+knowledge in concrete situations.
+
+The [UFrameIT](https://github.com/UFrameIT) framework uses the
+[Unity game engine](http://unity.com) with the [MMT](https://kwarc.info/projects/mmt)
+system. 
+
+*For students*: Topics for theses and projects are available [here](https://gl.kwarc.info/kwarc/thesis-projects/-/issues?label_name%5B%5D=FrameIT).

systems/jobad.md

@@ -5,6 +5,7 @@ title: JOBAD
 shorttitle: JOBAD
 teaser: A Javascrip Framework for instrumenting Active Documents with Semantic Services
 start_date: 2008-09
+end_date: 2015-12
 oprhan: true
 
 people: 

systems/kat.md

@@ -6,6 +6,7 @@ shorttitle: KAT
 teaser: An Annotation Tool for STEM Documents
 
 start_date: 2013-06
+end_date: 2017-06
 orphan: true
 
 people:

systems/mathhub.md

@@ -12,12 +12,14 @@ people:
     - akohlhase
     - cjucovschi
     - twiesing
+    - kbercic
 
 supported-by:
     - mathsearch
     - oaf
     - odk
     - latin
+    - mdh
 
 logo: public/mathHubLogo.png
 website: http://mathhub.info

systems/meta/historic.md

@@ -10,7 +10,7 @@ semantic wiki, mathematical web services, and invasive OMDoc editing
 technologies. Furthermore, the group works on the utilization of OMDoc to provide Logic
 Interoperability and to establish scientific Communities of Practice.
  
-{% assign systems = site.pages | where: "layout", "system" | sort: "pillar" | sort: "start_date" %}
+{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
 
 <ul class="collection">
     {% for item in systems %}

systems/meta/orphans.md

@@ -9,7 +9,7 @@ to greener pastures (e.g. when they graduate). We put these systems up for adopt
 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: "pillar" | sort: "start_date" %}
+{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
 
 <ul class="collection">
     {% for item in systems %}

systems/mmt.md

@@ -14,6 +14,7 @@ people:
     - miancu
     - fhorozal
     - mkohlhase
+    - nroux
 
 supported-by:
     - oaf

systems/mws.md

@@ -14,15 +14,15 @@ people:
     - cprodescu
     - rhambasan
     - ahambasan
-
+    - twiesing
 supported-by:
     - mathsearch
     - odk
+    - oaf
 
-
-logo: public/kwarc_logo.svg
+<!-- logo: public/kwarc_logo.svg -->
 website: http://search.mathweb.org
-repository: http://githhub.com/KWARC/mws
+repository: https://github.com/MathWebSearch
 publink: http://kwarc.github.io/bibs/mws
 ---
 
@@ -36,3 +36,10 @@ 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/sally.md

@@ -6,6 +6,7 @@ shorttitle: Sally
 teaser: A framework for mashing up semantic services into desktop applications.
 
 start_date: 2013-02
+start_date: 2016-08
 orphan: true
 
 people: 

systems/smglom.md

@@ -3,8 +3,7 @@ layout: system
 
 title: "SMGLoM - A Semantic, Multilingual Glossary of Mathematics"
 shorttitle: SMGLoM
-teaser: A terminological resource for Mathematics. 
-
+teaser: A terminological resource for Mathematics
 start_date: 2013-11
 
 people: 
@@ -18,16 +17,24 @@ supported-by:
     - mathsearch
     - odk
 logo: public/kwarc_logo.svg
-publink: http://kwarc.github.io/bibs/smglom
+publink: https://kwarc.github.io/bibs/smglom
 ---
-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/mh/glossary) and a [math dictionary](https://mathhub.info/mh/dictionary).
+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/smglom), and
-* [the sources on gl.mathhub.info](https://gl.mathhub.info/smglom), written in [sTeX](/systems/sTeX) (a semantic version of LaTeX.
+* [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](http://kwarc.info/kohlhase/papers/icms16-smglom.pdf) ICMS 2016
-* M. Kohlhase (2014) [*A data model and encoding for a semantic, multilingual terminology of mathematics*](http://kwarc.info/kohlhase/papers/cicm14-smglom.pdf) CICM 2014 
-* ... [complete bibliography](http://kwarc.github.io/bibs/smglom/)
-* [blue notes](http://gl.kwarc.info/smglom/blue): the epsilon-baked ideas about how to continue 
+* 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/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