more metadata

_includes/nav.html

-
 <!-- Navigation -->
 <nav class="navbar navbar-default  navbar-fixed-top">
   <div class="container" >

projects/FormalCAD.md

 ---
 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. 

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

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.

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. 

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)
 ---

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
 ---
 

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.

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.

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).

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.

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.

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.