From dd6251e94b8cd266ba1c405b15f8427f543a7b0f Mon Sep 17 00:00:00 2001 From: Michael Kohlhase <m.kohlhase@jacobs-university.de> Date: Sat, 6 May 2017 09:30:54 +0200 Subject: [PATCH] more projects --- projects/FormalCAD.md | 9 +++++++++ projects/jem.md | 9 +++++++++ projects/latin.md | 9 +++++++++ projects/logosphere.md | 15 +++++++++++++++ projects/mathsearch.md | 19 +++++++++++++++++++ projects/mws.md | 14 ++++++++++++++ projects/oaf.md | 10 ++++++++++ projects/odk.md | 10 ++++++++++ projects/omoc.md | 9 +++++++++ projects/once-cs.md | 9 +++++++++ projects/openmath-tn.md | 11 +++++++++++ projects/sissi.md | 9 +++++++++ projects/smglom.md | 9 +++++++++ projects/smglom.tex | 19 +++++++++++++++++++ 14 files changed, 161 insertions(+) create mode 100644 projects/FormalCAD.md create mode 100644 projects/jem.md create mode 100644 projects/latin.md create mode 100644 projects/logosphere.md create mode 100644 projects/mathsearch.md create mode 100644 projects/mws.md create mode 100644 projects/oaf.md create mode 100644 projects/odk.md create mode 100644 projects/omoc.md create mode 100644 projects/once-cs.md create mode 100644 projects/openmath-tn.md create mode 100644 projects/sissi.md create mode 100644 projects/smglom.md create mode 100644 projects/smglom.tex diff --git a/projects/FormalCAD.md b/projects/FormalCAD.md new file mode 100644 index 0000000..aba43ad --- /dev/null +++ b/projects/FormalCAD.md @@ -0,0 +1,9 @@ +--- +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 +--- diff --git a/projects/jem.md b/projects/jem.md new file mode 100644 index 0000000..6d64df9 --- /dev/null +++ b/projects/jem.md @@ -0,0 +1,9 @@ +--- +layout: project +menu_title: JEM +title: "JEM:JoiningEducationalMathematics" +pillar: KMR +start: 2006 +end: 2009 +people: mkohlhase +--- diff --git a/projects/latin.md b/projects/latin.md new file mode 100644 index 0000000..7a3d663 --- /dev/null +++ b/projects/latin.md @@ -0,0 +1,9 @@ +--- +layout: project +menu_title: LATIN +title: "LATIN: Logic Atlas & Integrator" +pillar: KMR +start: 2009 +end: 2012 +people: mkohlhase,frabe +--- diff --git a/projects/logosphere.md b/projects/logosphere.md new file mode 100644 index 0000000..047a006 --- /dev/null +++ b/projects/logosphere.md @@ -0,0 +1,15 @@ +--- +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. + diff --git a/projects/mathsearch.md b/projects/mathsearch.md new file mode 100644 index 0000000..6abf32a --- /dev/null +++ b/projects/mathsearch.md @@ -0,0 +1,19 @@ +--- +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/). diff --git a/projects/mws.md b/projects/mws.md new file mode 100644 index 0000000..9323427 --- /dev/null +++ b/projects/mws.md @@ -0,0 +1,14 @@ +--- +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). diff --git a/projects/oaf.md b/projects/oaf.md new file mode 100644 index 0000000..9e99016 --- /dev/null +++ b/projects/oaf.md @@ -0,0 +1,10 @@ +--- +layout: project +menu_title: OAF +title: "OAF: An Open Archive for Formalizations" +pillar: KMR +start: 2014 +end: 2018 +people: mkohlhase,frabe,dmueller +--- + diff --git a/projects/odk.md b/projects/odk.md new file mode 100644 index 0000000..f369f1c --- /dev/null +++ b/projects/odk.md @@ -0,0 +1,10 @@ +--- +layout: project +menu_title: OpenDreamKit +title: OpenDreamKit +pillar: KMR +start: 2015-09 +end: 2019-08 +people: mkohlhase,frabe,twiesing +--- + diff --git a/projects/omoc.md b/projects/omoc.md new file mode 100644 index 0000000..76da9d9 --- /dev/null +++ b/projects/omoc.md @@ -0,0 +1,9 @@ +--- +layout: project +menu_title: OMOC +title: "OMoC: Ontology-based Management of Change" +pillar: KMR +start: 2008 +end: 2010 +people: mkohlhase +--- diff --git a/projects/once-cs.md b/projects/once-cs.md new file mode 100644 index 0000000..9857ed9 --- /dev/null +++ b/projects/once-cs.md @@ -0,0 +1,9 @@ +--- +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 +--- diff --git a/projects/openmath-tn.md b/projects/openmath-tn.md new file mode 100644 index 0000000..e89dc57 --- /dev/null +++ b/projects/openmath-tn.md @@ -0,0 +1,11 @@ +--- +layout: project +menu_title: OpenMath TN +title: Thematic Netork "OpenMath" +pillar: KMR +start: 2003 +end: 2004 +funding: EU +program: Thematic Netork +people: mkohlhase +--- diff --git a/projects/sissi.md b/projects/sissi.md new file mode 100644 index 0000000..05f1067 --- /dev/null +++ b/projects/sissi.md @@ -0,0 +1,9 @@ +--- +layout: project +menu_title: SiSsI +title: "SiSsI: Software Engineering for Spreadsheet Interaction" +pillar: KMR +start: 2011 +end: 2013 +people: mkohlhase,akohlhase +--- diff --git a/projects/smglom.md b/projects/smglom.md new file mode 100644 index 0000000..cc835fd --- /dev/null +++ b/projects/smglom.md @@ -0,0 +1,9 @@ +--- +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 diff --git a/projects/smglom.tex b/projects/smglom.tex new file mode 100644 index 0000000..025fcf7 --- /dev/null +++ b/projects/smglom.tex @@ -0,0 +1,19 @@ +--- +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/). -- GitLab