X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fmembers%2Fkick-off.xml;h=5fd4d3e430a8edd1de82dd635c7f49a91cd7ffb5;hb=829cefe178cd633bb0c6deb18b29bba3e5e3bc16;hp=e02a683cdd8062b8b21108454e3f087c874c2f97;hpb=9db59fb2f254e37ae424d80cccd8ecc1c65ab6a8;p=helm.git
diff --git a/helm/mowgli/home/xml/members/kick-off.xml b/helm/mowgli/home/xml/members/kick-off.xml
index e02a683cd..5fd4d3e43 100644
--- a/helm/mowgli/home/xml/members/kick-off.xml
+++ b/helm/mowgli/home/xml/members/kick-off.xml
@@ -9,13 +9,19 @@
-
+
+
+
+
+
+
- A comparison of the aims and approaches of HELM and OpenMath.
+
+ A comparison of the aims and approaches of HELM and OpenMath.
+
-
- Presentation of the work of Sophia-Antipolis: Project Lemme;
- PCoq (an interface to the Coq system based on Aioli [for tree management],
- PPML [a sort of stylesheet language] and Figue [rendering engine]).
+
+
+
+ Presentation of the work of Sophia-Antipolis: Project Lemme;
+ PCoq (an interface to the Coq system based on Aioli [for tree management],
+ PPML [a sort of stylesheet language] and Figue [rendering engine]).
+
-
- Presentation of the work of Rocquencourt: Coq (proof assistant) and its
- problems:
-
- - Classification of theories:
-
- - Actually based only on the affiliation of the author.
- - We should have classifications based on subject, theme, author, etc.
-
-
- - Retrieving:
-
- - By pattern. Problem: the patterns (n < m+1) and (n <= m) are
- differents but denote the same thing.
- - By isomorphisms. Problem: we can capture just a few of them.
-
-
- - Proof Rendering in Natural Language: still too many detailed.
- Views at different levels of detail can probably help.
-
- - Modularity
-
+
+
+
+ Presentation of the work of Rocquencourt: Coq (proof assistant) and its
+ problems:
+
+ - Classification of theories:
+
+ - Actually based only on the affiliation of the author.
+ - We should have classifications based on subject, theme, author, etc.
+
+
+ - Retrieving:
+
+ - By pattern. Problem: the patterns (n < m+1) and (n <= m) are
+ differents but denote the same thing.
+ - By isomorphisms. Problem: we can capture just a few of them.
+
+
+ - Proof Rendering in Natural Language: still too many detailed.
+ Views at different levels of detail can probably help.
+
+ - Modularity
+
+
- Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
- planned contributions to MOWGLI.
+
+ Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
+ planned contributions to MOWGLI.
+
- Presentation of the projects in which he is envolved or that he is
- coordinating; interest in metadata; problems related to having papers
- in electronic form. His main contribution will be providing links to
- mathematicians.
+
+ Presentation of the projects in which he is envolved or that he is
+ coordinating; interest in metadata; problems related to having papers
+ in electronic form. His main contribution will be providing links to
+ mathematicians.
+
-
- Presentation of the work done at the Max Planck Institute for Gravitational
- Physics; presentation of Living Reviews in Relativity and expectations
- from MOWGLI (i.e. searching, rendering, interoperability). He points out
- how Living Reviews in Relativity already provide a notion of versioning;
- how hyperlinks are managed (often opening pop-ups). He finally presents
- some data that show that on-line browsing of papers really happens.
+
+
+
+ Presentation of the work done at the Max Planck Institute for Gravitational
+ Physics; presentation of Living Reviews in Relativity and expectations
+ from MOWGLI (i.e. searching, rendering, interoperability). He points out
+ how Living Reviews in Relativity already provide a notion of versioning;
+ how hyperlinks are managed (often opening pop-ups). He finally presents
+ some data that show that on-line browsing of papers really happens.
+
- Presentation of the work done at Trusted Logic. Brief introduction to
- the Common Criteria Software: lot of documentation must be produced for
- third (and fourth!) parties evaluation; formal evaluation is one goal
- (not yet reached). The main problems Trusted Logic meets are:
-
- - Presentation
- - Managing thousands of definitions/theorems and links between them
- - Evaluators needs: hiding/displaying information; different views on the
- same proofs/definitions; metadata; backpointers (which lemmas are
- used in a theorem)
- - Interoperability with other software tools
- - Proofs mantainance
-
- A final remark is that Trusted Logic is just interested in provability
- (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
- language description of them).
+
+ Presentation of the work done at Trusted Logic. Brief introduction to
+ the Common Criteria Software: lot of documentation must be produced for
+ third (and fourth!) parties evaluation; formal evaluation is one goal
+ (not yet reached). The main problems Trusted Logic meets are:
+
+ - Presentation
+ - Managing thousands of definitions/theorems and links between them
+ - Evaluators needs: hiding/displaying information; different views on the
+ same proofs/definitions; metadata; backpointers (which lemmas are
+ used in a theorem)
+ - Interoperability with other software tools
+ - Proofs mantainance
+
+ A final remark is that Trusted Logic is just interested in provability
+ (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
+ language description of them).
+
- Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
- (to encode mathematical documents) and/or MBase (to distribute mathematical
- documents) and metadata.
+
+ about the "Usability of MBase for MOWGLI"
+
+
+
+ Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
+ (to encode mathematical documents) and/or MBase (to distribute mathematical
+ documents) and metadata.
+
Whenever someone is going to make a talk, he must report this to him.