Skip to content
Snippets Groups Projects
Commit a33b6f4d authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

adding teasers

parent 47e1cd90
No related branches found
No related tags found
No related merge requests found
---
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
......
......@@ -2,6 +2,7 @@
layout: project
title: "LATIN: Logic Atlas & Integrator"
teaser: Building a theory graph of logic represesentations.
active: false
start_date: '2009'
......
......@@ -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
......
......@@ -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).
......@@ -9,6 +9,7 @@ end_date: '2008'
people:
- mkohlhase
- nmueller
funding: EU
program: FET
......
......@@ -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
......
......@@ -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 ...
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment