From a33b6f4decb6694721379717e2082f0ac714c349 Mon Sep 17 00:00:00 2001
From: Michael Kohlhase <m.kohlhase@jacobs-university.de>
Date: Sat, 24 Jun 2017 10:31:29 +0200
Subject: [PATCH] adding teasers
---
projects/jem.md | 7 +++++--
projects/latin.md | 1 +
projects/logosphere.md | 3 ++-
projects/omoc.md | 4 +++-
projects/once-cs.md | 1 +
projects/openmath-tn.md | 2 ++
research/structural-semantics.md | 6 +++++-
7 files changed, 19 insertions(+), 5 deletions(-)
diff --git a/projects/jem.md b/projects/jem.md
index 389b33c..4c656f4 100644
--- a/projects/jem.md
+++ b/projects/jem.md
@@ -1,14 +1,17 @@
---
layout: project
-title: "JEM: JoiningEducationalMathematics"
+title: "JEM: Joining Educational Mathematics"
+teaser: Coordination of European content enrichment activities in the area of mathematics
active: false
start_date: '2006'
end_date: '2009'
people:
- - mkohlhase
+ - mkohlhase
+ - nmueller
+ - cmueller
funding: EU
program: eContentPlus Thematic Network
diff --git a/projects/latin.md b/projects/latin.md
index e1f66c7..43d6a42 100644
--- a/projects/latin.md
+++ b/projects/latin.md
@@ -2,6 +2,7 @@
layout: project
title: "LATIN: Logic Atlas & Integrator"
+teaser: Building a theory graph of logic represesentations.
active: false
start_date: '2009'
diff --git a/projects/logosphere.md b/projects/logosphere.md
index 83df700..97d721a 100644
--- a/projects/logosphere.md
+++ b/projects/logosphere.md
@@ -2,6 +2,7 @@
layout: project
title: "Logosphere: Formal Digital Libraries"
+teaser: Integrating Theorem Prover Libraries through Meta-logical Frameworks
active: false
start_date: '2003'
@@ -13,7 +14,7 @@ people:
collaborators:
- Carsten Schürmann, Yale University
- Frank Pfenning, CMU
- - Natarajan Shankar
+ - Natarajan Shankar, SRI International
- Sam Owre, SRI International
funding: NSF
diff --git a/projects/omoc.md b/projects/omoc.md
index cef692f..1ef1d3a 100644
--- a/projects/omoc.md
+++ b/projects/omoc.md
@@ -2,6 +2,7 @@
layout: project
title: "OMoC: Ontology-based Management of Change"
+teaser: Using semantic features in document collections for better change management.
active: false
start_date: '2008'
@@ -9,6 +10,7 @@ end_date: '2010'
people:
- mkohlhase
+ - nmueller
collaborators:
- Dieter Hutter, DFKI Bremen
@@ -18,6 +20,6 @@ program: Normalverfahren
grantid: KO 2428/8-1
---
-The OMOC project studies mechanisms for the Ontology-based Management of Change
+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 432bb2a..49838c4 100644
--- a/projects/once-cs.md
+++ b/projects/once-cs.md
@@ -9,6 +9,7 @@ end_date: '2008'
people:
- mkohlhase
+ - nmueller
funding: EU
program: FET
diff --git a/projects/openmath-tn.md b/projects/openmath-tn.md
index a979371..d64a06f 100644
--- a/projects/openmath-tn.md
+++ b/projects/openmath-tn.md
@@ -2,6 +2,7 @@
layout: project
title: Thematic Netork "OpenMath"
+teaser: Integrating Math Software Systems by content Markup for Formulae
active: false
start_date: '2001'
@@ -9,6 +10,7 @@ end_date: '2004'
people:
- mkohlhase
+ - nmueller
funding: EU
program: IST Thematic Netork
diff --git a/research/structural-semantics.md b/research/structural-semantics.md
index ca7cbfe..7720fef 100644
--- a/research/structural-semantics.md
+++ b/research/structural-semantics.md
@@ -3,6 +3,10 @@ layout: page
title: Structural Semantics
menu_order: 103
---
-Computer support for document interaction is only possible, if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with formal methods. In many cases, useful services can be rendered by machines without having an entailment relation, for instance we can search for a formula, we can determine the concepts it depends upon, etc. The commonality of such services is that they are based on the structure of the formulae alone. For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
+
+Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with formal methods.
+In many cases, useful services can be rendered by machines without having an entailment relation, for instance we can search for a formula, we can determine the concepts it depends upon, etc.
+The commonality of such services is that they are based on the structure of the formulae alone.
+For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
...more to be written ...
--
GitLab