more projects

projects/FormalCAD.md

+---
+layout: project
+menu_title: FormalCAD
+title: "FormalCAD: Formal Methods and Semantic Technologies for Engineering Design Processes"
+pillar: KMR
+start: 2011
+end: 2012
+people: mkohlhase,cjucovschi
+---

projects/jem.md

+---
+layout: project
+menu_title: JEM
+title: "JEM:JoiningEducationalMathematics"
+pillar: KMR
+start: 2006
+end: 2009
+people: mkohlhase
+---

projects/latin.md

+---
+layout: project
+menu_title: LATIN
+title: "LATIN: Logic Atlas & Integrator"
+pillar: KMR
+start: 2009
+end: 2012
+people: mkohlhase,frabe
+---

projects/logosphere.md

+---
+layout: project
+menu_title: Logosphere
+title: "Logosphere: Formal Digital Libraries"
+pillar: KMR
+start: 2003
+end: 2004
+funding: NSF
+program: ITR
+people: mkohlhase
+collaborators: Carsten Schürmann (Yale University), Frank Pfenning (CMU) Natarajan Shankar, Sam Owre (SRI International)
+---
+
+Mathematical knowledge is at the core of science and engineering. The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing a Formal Digital Library called Logosphere, a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. Logosphere emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems. The Logosphere infrastructure is designed to be scalable with respect to the size of the knowledge base as well as the diversity of formalisms.
+

projects/mathsearch.md

+---
+layout: project
+menu_title: MathSearch
+title: "MathSearch: Analyse und Suche in mathematischen Formeln"
+pillar: KMR
+start: 2012
+end: 2015
+people: mkohlhase,dginev
+---
+
+The MathSearch Project develops a semantic search engine for mathematics in collaboration
+with the [ZBMath Group](https://zbmath.org/about/) at
+[FIZ Karlsruhe](https://www.fiz-karlsruhe.de/). It is funded by the
+[Leibniz Foundation](https://www.leibniz-gemeinschaft.de/) as SAW project
+AW-2012-FIZ_KA-2.
+
+We have deployed an instance of [MathWebSearch](/projects/mws/) engine as part of the
+[ZBMath Information System](http://zbmath.org) (see the "Formulae" tab there), and we have
+started the [SMGloM](/projects/smglom/).

projects/mws.md

+---
+layout: project
+menu_title: MathWebSearch
+title: "MathWebSearch a Mathematical Search Engine"
+pillar: KMR
+start: 2005
+people: mkohlhase,isucan,cprodescu,rhambasan,ahambasan
+---
+
+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).

projects/oaf.md

+---
+layout: project
+menu_title: OAF
+title: "OAF: An Open Archive for Formalizations"
+pillar: KMR
+start: 2014
+end: 2018
+people: mkohlhase,frabe,dmueller
+---
+

projects/odk.md

+---
+layout: project
+menu_title: OpenDreamKit
+title: OpenDreamKit
+pillar: KMR
+start: 2015-09
+end: 2019-08
+people: mkohlhase,frabe,twiesing
+---
+

projects/omoc.md

+---
+layout: project
+menu_title: OMOC
+title: "OMoC: Ontology-based Management of Change"
+pillar: KMR
+start: 2008
+end: 2010
+people: mkohlhase
+---

projects/once-cs.md

+---
+layout: project
+menu_title: ONCE-CS
+title: "ONCE-CS: Open Network of Centres of Excellence in Complex Systems"
+pillar: KMR
+start: 2005
+end: 2008
+people: mkohlhase
+---

projects/openmath-tn.md

+---
+layout: project
+menu_title: OpenMath TN
+title: Thematic Netork "OpenMath"
+pillar: KMR
+start: 2003
+end: 2004
+funding: EU
+program: Thematic Netork
+people: mkohlhase
+---

projects/sissi.md

+---
+layout: project
+menu_title: SiSsI
+title: "SiSsI: Software Engineering for Spreadsheet Interaction"
+pillar: KMR
+start: 2011
+end: 2013
+people: mkohlhase,akohlhase
+---

projects/smglom.md

+---
+layout: project
+menu_title: SMGloM
+title: "The Semantic, Multilingual Glossary of Mathematics"
+pillar: KMR
+start: 2013-11
+people: mkohlhase,cjucovshi,miancu
+---
+The [Semantic, Multilingual Glossary of Mathematics](/projects/smglom/) is a 

projects/smglom.tex

+---
+layout: project
+menu_title: MathSearch
+title: "The MathSearch Project"
+pillar: KMR
+start: 2012
+end: 2015
+people: mkohlhase,dginev
+---
+
+The MathSearch Project develops a semantic search engine for mathematics in collaboration
+with the [ZBMath Group](https://zbmath.org/about/) at
+[FIZ Karlsruhe](https://www.fiz-karlsruhe.de/). It is funded by the
+[Leibniz Foundation](https://www.leibniz-gemeinschaft.de/) as SAW project
+AW-2012-FIZ_KA-2.
+
+We have deployed an instance of [MathWebSearch](/projects/mws/) engine as part of the
+[ZBMath Information System](http://zbmath.org) (see the "Formulae" tab there), and we have
+started the [SMGloM](/projects/smglom/).