diff --git a/projects/jem.md b/projects/jem.md index 389b33ccc98f4896c386132c74a406d5d0ed40b3..4c656f4d6f13cf8932dfa8023c6818b3d554f3ee 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 e1f66c7842817d9b3a3f4d29ce6818aba9c4532d..43d6a4270f9e40e15894062e03d6445c73520f9e 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 83df700f95d4f5c7e818014f96fe208ba824f746..97d721a2f8102840db0cb9821c9510c42671c457 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 cef692f5aa4ec30b228bf76c6489e9b3ccf2a51e..1ef1d3a1c5b3db0a47cdca94a50d5151bc0d8dc6 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 432bb2a9548806ccdcd44c7d6e299086e3876f7c..49838c4358c5ab03257c747dd1b2d30edc76d0c5 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 a979371d32ee21b70d8c128e36ceb8543ba9043f..d64a06f99bbc1acb8217e845e1020bd93733900a 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 ca7cbfe3886e9163145b5c3ff03aadfddf170d2f..7720fef47e088634c26ab853b03f00b3d7f8fea3 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 ...