From b01f226e0295a7bb8c9f098b7cc66101f42e073c Mon Sep 17 00:00:00 2001
From: Michael Kohlhase <m.kohlhase@jacobs-university.de>
Date: Sat, 6 May 2017 10:45:44 +0200
Subject: [PATCH] more metadata
---
_includes/nav.html | 1 -
projects/FormalCAD.md | 16 ++++++++++++----
projects/README.md | 10 ++++++----
projects/jem.md | 6 ++++++
projects/latin.md | 20 ++++++++++++++++++--
projects/logosphere.md | 3 ++-
projects/mathsearch.md | 8 ++++++--
projects/oaf.md | 25 +++++++++++++++++++++++++
projects/odk.md | 6 ++++++
projects/omoc.md | 7 +++++++
projects/once-cs.md | 18 ++++++++++++++++++
projects/openmath-tn.md | 15 +++++++++++++--
projects/sissi.md | 30 +++++++++++++++++++++++++++---
13 files changed, 146 insertions(+), 19 deletions(-)
diff --git a/_includes/nav.html b/_includes/nav.html
index cc6829a..a0737b8 100644
--- a/_includes/nav.html
+++ b/_includes/nav.html
@@ -1,4 +1,3 @@
-
<!-- Navigation -->
<nav class="navbar navbar-default navbar-fixed-top">
<div class="container" >
diff --git a/projects/FormalCAD.md b/projects/FormalCAD.md
index aba43ad..60766de 100644
--- a/projects/FormalCAD.md
+++ b/projects/FormalCAD.md
@@ -1,9 +1,17 @@
---
layout: project
menu_title: FormalCAD
-title: "FormalCAD: Formal Methods and Semantic Technologies for Engineering Design Processes"
+title: "FormalCAD: Formal Methods and Semantic Technologies for Engineering Design
+Processes"
+teaser: Towards a computer-supported, document-oriented process for systematic engineering design and a semantic help system for CAD systems.
pillar: KMR
-start: 2011
-end: 2012
-people: mkohlhase,cjucovschi
+start: 2012-04
+end: 2015-02
+people: mkohlhase,akohlhase,cjucovschi
+funding: DFG
+program: Normalverfahren
+grantid: KO 2428/12-1
+collaborators: Lutz Schröder, FAU Erlangen.
---
+
+Systematic engineering design processes follow a series of standardized development stages that have many aspects in common with software engineering. In this analogy, CAD/CAM objects replace program code as the implementation stage of the development; however, other recognized development stages such as requirements or principle solutions are currently left largely informal and in fact are typically not laid down in machine-processable form at all. We propose to draw on the mentioned analogy and transfer methods from software engineering to engineering design in order to capture the full engineering design process formally and thus enhance in particular their reliability and reusability. We envision a document-oriented design process that integrates all stages of the development process from requirement specifications to CAD/CAM documents, and moreover incorporates background knowledge such as enterprise ontologies, industrial standards, and formalized geometric principles. In the FormalCAD project, we plan to develop the information architecture for such a process and support it with a tool that interfaces a CAD system with formal specification languages, ontology reasoners, and semantic document management systems, thus allowing for a comprehensive development methodology that supports completely formalized development strands, change and life-cycle management, as well as semantically interlinked semi-formal documents for documentation and certification. FormalCAD is a joint project with Prof.
diff --git a/projects/README.md b/projects/README.md
index 168b445..2933bed 100644
--- a/projects/README.md
+++ b/projects/README.md
@@ -8,10 +8,11 @@ Each post needs some specific parameters:
* **layout** use `project` or `software`
* **title** the title of the project
- * **subtitle** (optionnal) a subtitle. It will be adjuncted to your title in the post
+ * **subtitle** (optional) a subtitle. It will be adjuncted to your title in the post
link and just under the title in the post page
- * **people** the KWARC people involved in this
- * **collaborators** the outside collaborators
+ * **teaser** (optional) a one-line description for the overview
+ * **people** (optional) the KWARC people involved in this
+ * **collaborators** (optional) the outside collaborators
* **start** (optional) the project start date
* **end** (optional) the project end date
* **pillar** (optional) the pillar (in the sense of http://kwarc.info/research) of the
@@ -20,4 +21,5 @@ Each post needs some specific parameters:
link from old activities pages on the former site.
* **funding** (optional): the funding body, *DFG*, *Leibniz Foundation*, *EU*, *Industry*
* **program** (optional): the funding program
- * **fundid** (optional): the project identifier of the funder, e.g. `KO 2428/13-1`
+ * **grantid** (optional): the project identifier of the funder, e.g. `KO 2428/13-1`
+ * **url** (optional): the project home page
diff --git a/projects/jem.md b/projects/jem.md
index 6d64df9..a53d599 100644
--- a/projects/jem.md
+++ b/projects/jem.md
@@ -5,5 +5,11 @@ title: "JEM:JoiningEducationalMathematics"
pillar: KMR
start: 2006
end: 2009
+funding: EU
+program: eContentPlus Thematic Network
+url: http://calc.mathstat.helsinki.fi/jem/en/about/
people: mkohlhase
---
+The network assembles leading developers of semantic web technologies for the
+representation of mathematics, mathematics content stakeholders and experienced
+distributors of software and eLearning solutions.
diff --git a/projects/latin.md b/projects/latin.md
index 7a3d663..ede1592 100644
--- a/projects/latin.md
+++ b/projects/latin.md
@@ -2,8 +2,24 @@
layout: project
menu_title: LATIN
title: "LATIN: Logic Atlas & Integrator"
-pillar: KMR
+pillar: foundations
start: 2009
end: 2012
-people: mkohlhase,frabe
+funding: DFG
+program: Normalverfahren
+grantid: KO 2428/9-1
+people: mkohlhase,frabe,fhorozal,miancu
+collaborators: Till Mossakowski, DFKI Bremen
---
+
+LATIN aims at developing methods, techniques, and tools for interfacing logics and proof
+systems. Logics allow making the mathematical knowledge at the core of science,
+engineering, and economics accessible to computational systems like (semi-)automated
+theorem provers, model checkers, computer algebra systems, constraint solvers, or concept
+classifiers. Unfortunately, these systems have differing foundational assumptions and
+input languages, which makes them non-interoperable and difficult to compare and evaluate
+in practice.The LATIN project focuses on developing a foundationally unconstrained
+framework for knowledge representation that allows to represent the meta-theoretic
+foundations of the mathematical knowledge in the same format and to interlink the
+foundations at the meta-logical level. This approach of logics as theories leads to
+interoperability of both system behavior and represented knowledge.
diff --git a/projects/logosphere.md b/projects/logosphere.md
index 047a006..3d2e47b 100644
--- a/projects/logosphere.md
+++ b/projects/logosphere.md
@@ -4,9 +4,10 @@ menu_title: Logosphere
title: "Logosphere: Formal Digital Libraries"
pillar: KMR
start: 2003
-end: 2004
+end: 2006
funding: NSF
program: ITR
+grantid: CCR-ITR-0325808
people: mkohlhase
collaborators: Carsten Schürmann (Yale University), Frank Pfenning (CMU) Natarajan Shankar, Sam Owre (SRI International)
---
diff --git a/projects/mathsearch.md b/projects/mathsearch.md
index 6abf32a..6ace201 100644
--- a/projects/mathsearch.md
+++ b/projects/mathsearch.md
@@ -2,9 +2,13 @@
layout: project
menu_title: MathSearch
title: "MathSearch: Analyse und Suche in mathematischen Formeln"
+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.
pillar: KMR
-start: 2012
-end: 2015
+start: 2012-03
+end: 2015-02
+funding: Leibniz Foundation
+program: SAW
+grantid: SAW-2012-FIZ_KA-2
people: mkohlhase,dginev
---
diff --git a/projects/oaf.md b/projects/oaf.md
index 9e99016..85ebb88 100644
--- a/projects/oaf.md
+++ b/projects/oaf.md
@@ -2,9 +2,34 @@
layout: project
menu_title: OAF
title: "OAF: An Open Archive for Formalizations"
+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.
pillar: KMR
start: 2014
end: 2018
+funding: DFG
+program: Normalverfahren
+grantid: KO 2428/13-1
people: mkohlhase,frabe,dmueller
---
+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.
+
+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,
+constructive type theory, etc.), library formats, and library structures, and much work is
+spent developing basic libraries for mathematics in each system. Moreover, the ensuing
+plurality of library formats forces implementors to spend time developing library
+organization features (e.g., distribution, browsing, search, change management) for each
+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
+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
+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.
diff --git a/projects/odk.md b/projects/odk.md
index f369f1c..3a7deb5 100644
--- a/projects/odk.md
+++ b/projects/odk.md
@@ -5,6 +5,12 @@ title: OpenDreamKit
pillar: KMR
start: 2015-09
end: 2019-08
+funding: EU
+program: Research Infrastructure
+grantid: #676541
+url: http://opendreamkit.org
people: mkohlhase,frabe,twiesing
---
+OpenDreamKit is a Horizon 2020 European Research Infrastructure project (#676541) that will run for four years, starting from September 2015. It provides substantial funding to the open source computational mathematics ecosystem, and in particular popular tools such as LinBox, MPIR, SageMath, GAP, Pari/GP, LMFDB, Singular, MathHub, and the IPython/Jupyter interactive computing environment.
+From this ecosystem, OpenDreamKit will deliver a flexible toolkit enabling research groups to set up Virtual Research Environments, customised to meet the varied needs of research projects in pure mathematics and applications, and supporting the full research life-cycle from exploration, through proof and publication, to archival and sharing of data and code.
diff --git a/projects/omoc.md b/projects/omoc.md
index 76da9d9..e6af448 100644
--- a/projects/omoc.md
+++ b/projects/omoc.md
@@ -5,5 +5,12 @@ title: "OMoC: Ontology-based Management of Change"
pillar: KMR
start: 2008
end: 2010
+funding: DFG
+program: Normalverfahren
+grantid: KO 2428/8-1
+collaborators: Dieter Hutter, DFKI Bremen
people: mkohlhase
---
+The OMOC project studies mechanisms for the Ontology-based Management of Change
+The idea is to manage dependencies in/between documents (given by document ontology). The
+target is collaborative editing of mathematical documents (Plugin to Version Control).
diff --git a/projects/once-cs.md b/projects/once-cs.md
index 9857ed9..293067a 100644
--- a/projects/once-cs.md
+++ b/projects/once-cs.md
@@ -5,5 +5,23 @@ title: "ONCE-CS: Open Network of Centres of Excellence in Complex Systems"
pillar: KMR
start: 2005
end: 2008
+funding: EU
+program: FET
people: mkohlhase
---
+
+The science of complex systems is crucial to FET and the economic success of Europe. But
+complex systems research is still not well coordinated in Europe, with urgent need to
+connect and expand the community. This three-year CA coordinates and integrates scientific
+research and dissemination in the European CS community by (i) identifying fundamental
+questions across CS in all areas of application, in order to ground the new science, (ii)
+encouraging and facilitating research collaboration around the fundamental questions, to
+stimulate research and applications across academic disciplines, industry and government,
+(iii) establishing sustainable cross-disciplinary education in CS science, (iv)
+coordinating the creation of a European PhD in CS science, (v) supporting European Centres
+of Excellence in CS science, (vi) providing network infrastructure for the new Integrated
+Projects and connecting them and the CS community, and (vii) coordinating the formation of
+a vigorous self-sustaining European Complex Systems Society (ECSS), to take over the
+networking and coordinating roles of Exystence and ONCE-CS. All this is enabled by (viii)
+the provision of a robust and well-designed Internet portal providing many delivery,
+retrieval, communication, and management services.
diff --git a/projects/openmath-tn.md b/projects/openmath-tn.md
index e89dc57..596c543 100644
--- a/projects/openmath-tn.md
+++ b/projects/openmath-tn.md
@@ -3,9 +3,20 @@ layout: project
menu_title: OpenMath TN
title: Thematic Netork "OpenMath"
pillar: KMR
-start: 2003
+start: 2001
end: 2004
funding: EU
-program: Thematic Netork
+program: IST Thematic Netork
+grantid: IST-2000-29719
+url: http://www.openmath.org/projects/thematic/
people: mkohlhase
---
+The OpenMath Thematic Network, was a European Union sponsored project with the following
+main activities:
+
+ * to organise workshops bringing together people working on OpenMath from around the world;
+ * to provide a continued focus-point for the development of the OpenMath Standard and Content Dictionaries;
+ * to facilitate European participation in the W3C Math Working group by sponsoring the representatives from NAG, Stilo Technology and INRIA.
+ * to coordinate the development of OpenMath and MathML tools, in particular stylesheets;
+ * to coordinate the development of OpenMath and MathML applications;
+ * to disseminate information about OpenMath and MathML.
diff --git a/projects/sissi.md b/projects/sissi.md
index 05f1067..4edb638 100644
--- a/projects/sissi.md
+++ b/projects/sissi.md
@@ -2,8 +2,32 @@
layout: project
menu_title: SiSsI
title: "SiSsI: Software Engineering for Spreadsheet Interaction"
+teaser: Methods and technologies to enhance spreadsheets semantically.
pillar: KMR
-start: 2011
-end: 2013
-people: mkohlhase,akohlhase
+start: 2011-08
+end: 2013-07
+funding: DFG
+program: Normalverfahren
+grantid: KO 2428/10-1
+collaborators: Dr. Dieter Hutter, DFKI Bremen
+people: mkohlhase,akohlhase,cjucovschi
---
+
+Spreadsheets have become very popular to analyze and visualize business and science data,
+so their complexity and impact increased dramatically over the years. As active documents
+they are situated somewhere between software systems and documents. Nevertheless,
+spreadsheets are still largely written by end users in an informal process, lacking
+typically any abstract operational model, any sufficient verification or testing of their
+behavior, and any appropriate user assistance for their readers. Thus, existing
+spreadsheets are subject to high error rates as well as high-impact
+misinterpretations. The proposed project therefore aims at the development of a
+semantic-based framework to provide
+
+ 1. abstract modeling, refinement, and knowledge management techniques for spreadsheets
+ 2. verification and consistent evolution of spreadsheets as well as their usage as interfaces to data bases,
+ 3. interpretation and views for spreadsheets as document-centered user assistance.
+
+The central claim to be tested in the SISsI project is that we can employ synergies
+between software engineering and user assistance at two levels: they can share the
+knowledge model, and they can share a user interface whose primary functionality is to
+relate spreadsheet content with spreadsheet layout to enable innovative interactions.
--
GitLab