projects/comma.md

+---
+layout: project
+
+title: "CoMMa: Corpus Meta-Mathematics"
+shorttitle: CoMMa
+active: true
+teaser: Representing and Extracting the Meaning of Mathematical/Technical Documents
+start_date: '2006'
+funding: internal
+
+people:
+    - mkohlhase
+    - dginev
+    - jfschaefer
+    - pzoleko
+logo: public/kwarc_logo.svg
+publink: auto
+funding: internal
+---
+
+Many of the foundations of the wealth of western societies are laid down in mathematical/technical documents. Such are rich in structure and communicate complex meaning effectively and efficiently, but we do not understand the underlying knowledge structures and linguistic characteristics enough to extract the underlying meanings and represent them explicitly enough so that working with them can be supported by machines.
+
+This leads to the [one brain barrier](/kohlhase/papers/ems13.pdf) in Science, Technology, Engineering, and Mathematics (STEM): instead of being machine-processable, mathematical/technical knowledge must always pass through a human brain for innovation, application, and education. 
+In the CoMMa project, we work towards remedying this problem for Mathematics (which can serve as a test tube for STEM documents) by applying methods from
+
+##### Meta-Mathematics
+
+i.e. employing languages that allow to talk about the concepts, objects, and models of mathematics. We employ the [OMDoc (Open Mathematical Documents)](/systems/OMDoc/) format for representing document and knowledge structures at all levels and with flexible formality, the [MMT system](/systems/mmt) for formalizing knowledge in a foundation-independent manner ([details and discussion](http://kwarc.info/kohlhase/papers/omdoc-semantics.pdf)).
+
+##### Corpus-Linguistics
+
+i.e. extracting meaning-carrying structures from documents at the scale of large, representative corpora. We prepare and manage large mathematical corpora in the [arXMLiv effort](/projects/arXMLiv/) and distribute math linguistic data sets via the [SIGMathLing initiative](http://sigmathling.kwarc.info). We contribute to the infrastructure for math linguistics with the [LLaMaPUn](/systems/llamapun/) library and the [KAT](/systems/kat/) annotation tool.
+

projects/direga.md

+---
+layout: project
+title: "Digitaler Registerassistent"
+shorttitle: "DiRegA"
+teaser: Towards automating Register Courts via Symbolic and Subsymbolic AI
+
+active: true
+start_date: 'March 2024'
+end_date: 'February 2027'
+publink: auto
+
+people: 
+    - mkohlhase
+    - mrapp
+    - jfschaefer
+funding: Bundesnotarkammer
+logo: public/bnotk.jpg
+website: https://www.direga.fau.de/
+---
+The DIREGA ( Digitaler Registerassistent) project conducts muti-disciplinary, foundational
+research in Computer Science and the law. It studies the question if - and so how - legal
+decisions can be supported - and even be automated - by symbolic AI and machine
+learning. The legal application domain is register law. 
+
+The project is funded by the German Federal Chamber of Notaries (Bundesnotarkammer) in
+coorpation with the Bavarian Chamber of Notaries (Bayrische Notarkammer) and the Bavarian
+State Ministry of Justice (Bayerischen Staatsministerium der Justiz).
+
+For details (in German) see https://www.direga.fau.de/

projects/jem.md

@@ -2,17 +2,20 @@
 layout: project
 
 title: "JEM: Joining Educational Mathematics"
+shorttitle: JEM
 teaser:  Coordination of European content enrichment activities in the area of mathematics
 
 active: false
 start_date: '2006'
 end_date: '2009'
+publink: auto
 
 people:
     - mkohlhase 
     - nmueller 
     - cmueller 
 
+logo: public/eu_logo.png
 funding: EU
 program: eContentPlus Thematic Network
 

projects/latin.md

@@ -2,11 +2,13 @@
 layout: project
 
 title: "LATIN: Logic Atlas & Integrator"
+shorttitle: LATIN
 teaser: Building a theory graph of logic represesentations. 
 
 active: false
 start_date: '2009'
 end_date: '2012'
+publink: auto
 
 people: 
     - mkohlhase
@@ -17,6 +19,7 @@ people:
 collaborators:
     - Till Mossakowski, DFKI Bremen
 
+logo: public/dfg_logo.svg
 funding: DFG
 program: Normalverfahren
 grantid: KO 2428/9-1

projects/logosphere.md

@@ -2,11 +2,13 @@
 layout: project
 
 title: "Logosphere: Formal Digital Libraries"
+shorttitle: Logosphere
 teaser: Integrating Theorem Prover Libraries through Meta-logical Frameworks
 
 active: false
 start_date: '2003'
 end_date: '2006'
+publink: auto
 
 people:
     - mkohlhase

projects/mamored.md

@@ -2,10 +2,12 @@
 layout: project
 
 title: MaMoReD
+shorttitle: MaMoReD
 teaser: Flexiformalizing Mathematical Models as Research Data
 
 active: true
 start_date: '2016-11'
+publink: http://kwarc.github.io/bibs/MaMoReD
 
 people:
     - mkohlhase
@@ -15,10 +17,47 @@ people:
 
 collaborators:
     - Dr. Thomas Koprucki (WIAS Berlin)
-    - Dr. Karsten Tabelov (WIAS Berlin)
-
+    - Dr. Wolfram Sperber (FIZ Karlsruhe)
+    - Dr. Karsten Tabelow (WIAS Berlin)
+    - Dr. Olaf Teschke (FIZ Karlsruhe)
+logo: public/kwarc_logo.svg
 funding: internal
 ---
 The MaMoReD projects studies whether and how the flexiformalization of mathematical
 mathematical models can allow them to be treated as research data, i.e. to be amenable to
 mathematical knowledge management methods. 
+
+### Workshops
+
+<!-- don't introduce new lines here, it confuses the markdown processor; add two spaces at the end of a line for a line break -->
+
+1. 2018, January, 15-17 in Erlangen  
+   **Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow  
+   **Topics**  
+   * stochastic models (continued)
+   * preparation of grant proposal
+1. 2017, November, 4-8 at WIAS Berlin  
+   **Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow  
+   **Topics**  
+   * generation of Python and C code from MMT formalizations of models
+   * formal language for solution strategies of mathematical models
+   * stochastic models
+1. 2017, March, 21-24 at WIAS Berlin  
+   **Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow, Teschke  
+   **Topics**  
+   * preparation of journal paper on abstract definition of models
+   * formalization of units and quantities in MMT
+1. 2017, January, 16-19 in Erlangen  
+   **Participants**: Kohlhase, Koprucki, Müller, Rabe, Tabelow  
+   **Topics**  
+   * MMT tutorial
+   * formalization of van Roesbroock Modell for charge transport in semi-conductors in MMT
+   * formalizing complex device geometries
+   * survey of state of the art in mathematical modeling
+   * generation of LaTeX documents from MMT formalizations of models
+   1. 2016, November 9. at WIAS Berlin
+   **Participants**: Kohlhase, Koprucki, Tabelow
+   **Topics**
+   * Models as Research Data   
+   * Theory Graphs and Models
+   * Mathematical Knowledge Management for Models

projects/mathsearch.md

@@ -3,16 +3,19 @@ layout: project
 
 
 title: "MathSearch: Analyse und Suche in mathematischen Formeln"
+shorttitle: MathSearch
 teaser: Methods for information extraction and information retrieval for mathematical documents with the aim of providing semantically enhanced interaction for Zentralblatt Math and the arXiv.
 
 active: false
 start_date: 2012-03
 end_date: 2015-02
+publink: auto
 
 people: 
     - mkohlhase
     - dginev
 
+logo: public/leibniz_logo.svg
 funding: Leibniz Foundation
 program: SAW
 grantid: SAW-2012-FIZ_KA-2

projects/mdh.md

+---
+layout: project
+
+title: MathDataHub
+shorttitle: MDH
+teaser: A Collaboration Project with Ljubljana University
+
+active: false  
+start_date: 2020-01
+end_date: 2021-12
+
+people:
+    - mkohlhase
+    - frabe
+    - kbercic
+    - twiesing
+
+funding: DAAD
+program: Collaboration Grant
+logo: public/daad_logo.svg
+---
+Modern mathematical research increasingly depends on collaborative tools, computational environments, and online databases, and these are changing the way mathematical research is conducted and how it is turned into applications. For example, engineers now use mathematical tools to build and simulate physical models based on systems of differential equations with millions of variables, combining building blocks and algorithms taken from libraries shared all over the internet.
+The KWARC group at FAU Erlangen-Nürnberg and the group at Ljubljana University collaborate on the establishment of MathDataHub, a semantic portal for mathematical data sets. 

projects/meta/README.md

@@ -9,8 +9,11 @@ Each post needs some specific parameters:
  * **layout** use `project`
 
  * **title** the title of the project
+ * **shorttitle** the short title of the project, used for project chips
  * **teaser** (optional) a one-line description for the overview
 
+  * **logo** (optional) a (local) path to the logo of a project
+
  * **active** boolean indicating if the project is active
  * **start_date** the system start date (YYYY[-MM])
  * **end_date** (optional) the system end date (YYYY[-MM])

projects/meta/completed.md

@@ -10,7 +10,7 @@ permalink: /projects/completed/
 
 <ul class="collection">
     {% for item in projects %}
-       {% if item.funding %} {% include psitem.html %} {% endif %}
+       {% if item.funding %} {% include psitem.html item=item %} {% endif %}
     {% endfor %}
 </ul>
 
@@ -19,7 +19,7 @@ We also organize some of our research and development into Projects,
 
 <ul class="collection">
     {% for item in projects %}
-       {% unless item.funding %} {% include psitem.html %} {% endunless %}
+       {% unless item.funding %} {% include psitem.html item=item %} {% endunless %}
     {% endfor %}
 </ul>
 

projects/meta/index.md

@@ -11,7 +11,7 @@ permalink: /projects/
 <ul class="collection">
     {% for item in projects %}
         {% unless item.funding == 'internal' %}
-            {% include psitem.html %}
+            {% include psitem.html item=item %}
         {% endunless %}
     {% endfor %}
 </ul>
@@ -24,7 +24,7 @@ external researchers:
 <ul class="collection">
     {% for item in projects %}
         {% if item.funding == 'internal' %}
-            {% include psitem.html %}
+            {% include psitem.html item=item %}
         {% endif %}
     {% endfor %}
 </ul>

projects/oaf.md

@@ -2,25 +2,36 @@
 layout: project
 
 title: "OAF: An Open Archive for Formalizations"
+shorttitle: OAF
 teaser: The OAF Project builds a theoretical framework for interoperability of theorem prover libraries and implements an information system that host and align multiple libraries in a joint semantic setting.
 
-active: true
+active: false
 start_date: '2014'
-end_date: '2018'
+end_date: 'June 2020'
+publink: auto
 
 people: 
     - mkohlhase
     - frabe
     - dmueller
-
+    - jbetzendahl
+    - kamann
+    - jsee
+    - rmarcus
+    - mrupprecht
+    - aschmidt
+logo: public/dfg_logo.svg
 funding: DFG
 program: Normalverfahren
-grantid: KO 2428/13-1
+grantid: KO 2428/13-1, RA 18723/1-1
+proposal: http://kwarc.info/kohlhase/projects/oaf.pdf
 ---
 
-OAF is a DFG-funded research project running from 2014-2017 and headed by Michael Kohlhase
-and Florian Rabe at Jacobs University Bremen. It aims at the integration of formal
-mathematical libraries.
+OAF was a DFG-funded research project running from 2014-2020 and headed by Michael Kohlhase
+and Florian Rabe originally at Jacobs University Bremen and later at FAU Erlangen-Nürnberg.
+It centered on the integration of formal mathematical libraries.
+
+Both the [original proposal](http://kwarc.info/kohlhase/projects/oaf.pdf) and the [final report](../oaf-report.pdf) are available.
 
 Formal/symbolic systems and their libraries are non-interoperable because they are based
 on differing, mutually incompatible foundations (e.g., set theory, higher-order logic,
@@ -31,11 +42,11 @@ organization features (e.g., distribution, browsing, search, change management)
 library format. All these investments bind resources that could be used to improve the
 core functionality of the systems and the scope of the libraries.
 
-The OAF project tackles these interoperability and plurality problems by developing an
+The OAF project tackled these interoperability and plurality problems by developing an
 open archive for formalizations, a common and open infrastructure for managing and sharing
 formalized mathematical knowledge such as theories, definitions, and proofs.  The OAF
 infrastructure is designed to be scalable with respect to both the size of the knowledge
-base and the diversity of logical foundations. In particular, the OAF system will be based
+base and the diversity of logical foundations. In particular, the OAF system is based
 on a uniform foundation-independent representation format for libraries, which allows
 formalizing the logical foundations alongside the libraries and thus acts as framework for
 aligning libraries.

projects/odk.md

@@ -2,11 +2,14 @@
 layout: project
 
 title: OpenDreamKit
+shorttitle: ODK
 teaser: Towards an Open Virtual Research Environment Framework for (Computational) Mathematics.
 
-active: true
 start_date: 2015-09
 end_date: 2019-08
+active: false
+publink: http://kwarc.github.io/bibs/odk
+
 
 people:
     - mkohlhase
@@ -15,11 +18,20 @@ people:
     - miancu
     - cmaeder
     - dmueller
+    - tpollinger
+    - kbercic
+    - swille
+    - kamann
+    - jsee
+    - rmarcus
+    - mrupprecht
 
+logo: public/eu_logo.png
 funding: EU
 program: Research Infrastructure
 grantid: 676541
-
+logo: public/odk_logo.png
+proposal: https://github.com/OpenDreamKit/OpenDreamKit/blob/master/Proposal/proposal-www.pdf
 website: http://opendreamkit.org
 ---
 

projects/omoc.md

@@ -2,11 +2,13 @@
 layout: project
 
 title: "OMoC: Ontology-based Management of Change"
+shorttitle: OMoC
 teaser: Using semantic features in document collections for better change management. 
 
 active: false
 start_date: '2008'
 end_date: '2010'
+publink: auto
 
 people:
     - mkohlhase
@@ -15,6 +17,7 @@ people:
 collaborators:
     - Dieter Hutter, DFKI Bremen
 
+logo: public/dfg_logo.svg
 funding: DFG
 program: Normalverfahren
 grantid: KO 2428/8-1

projects/once-cs.md

@@ -2,16 +2,19 @@
 layout: project
 
 title: "ONCE-CS: Open Network of Centres of Excellence in Complex Systems"
+shorttitle: ONCE-CS
 teaser: Adding a Semantic Angle to Complex Systems
 
 active: false
 start_date: '22005'
 end_date: '2008'
+publink: auto
 
 people:
     - mkohlhase
     - nmueller
 
+logo: public/eu_logo.png
 funding: EU
 program: FET
 ---

projects/openmath-tn.md

@@ -2,6 +2,7 @@
 layout: project
 
 title: Thematic Netork "OpenMath"
+shorttitle: TN "OpenMath"
 teaser: Integrating Math Software Systems by content Markup for Formulae
 
 active: false
@@ -12,6 +13,7 @@ people:
     - mkohlhase
     - nmueller
 
+logo: public/eu_logo.png
 funding: EU
 program: IST Thematic Netork
 grantid:  IST-2000-29719

projects/sissi.md

@@ -2,11 +2,13 @@
 layout: project
 
 title: "SiSsI: Software Engineering for Spreadsheet Interaction"
+shorttitle: SiSsI
 teaser: Methods and technologies to enhance spreadsheets semantically.
 
 active: false
 start_date: 2011-08
 end_date: 2013-07
+publink: auto
 
 people: 
     - mkohlhase
@@ -16,6 +18,7 @@ people:
 collaborators:
     - Dr. Dieter Hutter, DFKI Bremen
 
+logo: public/dfg_logo.svg
 funding: DFG
 program: Normalverfahren
 grantid: KO 2428/10-1

projects/tetrapod.md → projects/tetrapod/index.md

@@ -2,23 +2,45 @@
 layout: project
 
 title: Tetrapod
+shorttitle: Tetrapod
 teaser: All four dimensions of Mathematical Knowledge Processing
 
 active: true
 start_date: '2011-12'
+publink: auto
 
 people:
     - mkohlhase
     - dmueller
     - frabe
+    - kbercic
 
 collaborators:
-    - Prof. William Farmer (McMaster University)
-    - Prof. Jacques Carette (McMaster University) 
+    - Prof. William Farmer (McMaster Univ.)
+    - Prof. Jacques Carette (McMaster Univ.) 
+    - Jasmine Sharoda (McMaster Univ.)
 
+logo: public/kwarc_logo.svg
 funding: internal
 ---
 
 The aim of the Tetrapod project is to produce tools for **trustworthy and efficient
   modeling** of problems involving mathematics as well as tools for doing **mathematical
   knowledge processing**.
+
+The main result of the project is the conception of a "doing math" involves four primary aspects
+
+* **computation** (which produces **information**),
+* **reasoning** (which produces **arguments**),
+* **tabulation** (which produces **data**),
+* **narration** (which produces **documents**),
+
+that are joined by a fifth, which binds them together: 
+
+* **organisation** (which produces **ontologies**).
+
+All in all we propose that these five aspects can be arranged in a tetrapodal structure
+
+<img alt="the tetrapod image for the five aspects of doing mathematics" src="tetrapod-arms.svg"/>
+
+Feel free to include this image into your paper via the [tikz sources provided here](tetrapod-arms.tex)