<!ATTLIST entry
author CDATA #IMPLIED>
- <!ELEMENT presentation (#PCDATA|ul)*>
+ <!ELEMENT presentation (slides*,description)>
<!ATTLIST presentation
media (blackboard|slides) #REQUIRED
- slides CDATA #IMPLIED
site CDATA #REQUIRED
author CDATA #REQUIRED>
+ <!ELEMENT description (#PCDATA|ul)*>
+
+ <!ELEMENT slides (#PCDATA)>
+ <!ATTLIST slides
+ file CDATA #REQUIRED
+ format (PowerPoint|PS|PDF|HTML) #REQUIRED>
+
<!ELEMENT participant (#PCDATA)>
<!ATTLIST participant
site CDATA #REQUIRED
<participant site="aei" file="weyher"/>
<participant site="aei" file="pollney"/>
<presentation site="bologna" author="asperti" media="blackboard">
- A comparison of the aims and approaches of HELM and OpenMath.
+ <description>
+ A comparison of the aims and approaches of HELM and OpenMath.
+ </description>
</presentation>
- <presentation site="inria" author="pottier"
- media="slides" slides="kick-off/lemme2.ppt">
- 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 site="inria" author="pottier" media="slides">
+ <slides file="kick-off/lemme2.ppt" format="PowerPoint"/>
+ <description>
+ 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]).
+ </description>
</presentation>
- <presentation site="inria" author="herbelin"
- media="slides" slides="kick-off/MoWGLI-LogiCal.ps">
- Presentation of the work of Rocquencourt: Coq (proof assistant) and its
- problems:
- <ul>
- <li>Classification of theories:
- <ul>
- <li>Actually based only on the affiliation of the author.</li>
- <li>We should have classifications based on subject, theme, author, etc.</li>
- </ul>
- </li>
- <li>Retrieving:
- <ul>
- <li>By pattern. Problem: the patterns (n < m+1) and (n <= m) are
- differents but denote the same thing.</li>
- <li>By isomorphisms. Problem: we can capture just a few of them.</li>
- </ul>
- </li>
- <li>Proof Rendering in Natural Language: still too many detailed.
- Views at different levels of detail can probably help.
- </li>
- <li>Modularity</li>
- </ul>
+ <presentation site="inria" author="herbelin" media="slides">
+ <slides file="kick-off/MoWGLI-LogiCal.ps" format="PS"/>
+ <description>
+ Presentation of the work of Rocquencourt: Coq (proof assistant) and its
+ problems:
+ <ul>
+ <li>Classification of theories:
+ <ul>
+ <li>Actually based only on the affiliation of the author.</li>
+ <li>We should have classifications based on subject, theme, author, etc.</li>
+ </ul>
+ </li>
+ <li>Retrieving:
+ <ul>
+ <li>By pattern. Problem: the patterns (n < m+1) and (n <= m) are
+ differents but denote the same thing.</li>
+ <li>By isomorphisms. Problem: we can capture just a few of them.</li>
+ </ul>
+ </li>
+ <li>Proof Rendering in Natural Language: still too many detailed.
+ Views at different levels of detail can probably help.
+ </li>
+ <li>Modularity</li>
+ </ul>
+ </description>
</presentation>
<presentation site="nijmegen" author="geuvers" media="slides">
- Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
- planned contributions to MOWGLI.
+ <slides file="mowgligroup.html" format="HTML"/>
+ <description>
+ Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
+ planned contributions to MOWGLI.
+ </description>
</presentation>
<presentation site="aei" author="wegner" media="blackboard">
- 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.
+ <description>
+ 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.
+ </description>
</presentation>
- <presentation site="aei" author="schutz"
- media="slides" slides="kick-off/AIP_Intro.ppt">
- 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 site="aei" author="schutz" media="slides">
+ <slides file="kick-off/AIP_Intro.ppt" format="PowerPoint"/>
+ <description>
+ 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.
+ </description>
</presentation>
<presentation site="trusted-logic" author="gimenez" media="blackboard">
- 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:
- <ul>
- <li>Presentation</li>
- <li>Managing thousands of definitions/theorems and links between them</li>
- <li>Evaluators needs: hiding/displaying information; different views on the
- same proofs/definitions; metadata; backpointers (which lemmas are
- used in a theorem)</li>
- <li>Interoperability with other software tools</li>
- <li>Proofs mantainance</li>
- </ul>
- 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).
+ <description>
+ 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:
+ <ul>
+ <li>Presentation</li>
+ <li>Managing thousands of definitions/theorems and links between them</li>
+ <li>Evaluators needs: hiding/displaying information; different views on the
+ same proofs/definitions; metadata; backpointers (which lemmas are
+ used in a theorem)</li>
+ <li>Interoperability with other software tools</li>
+ <li>Proofs mantainance</li>
+ </ul>
+ 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).
+ </description>
</presentation>
<presentation site="dfki" author="moschner" media="slides">
- Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
- (to encode mathematical documents) and/or MBase (to distribute mathematical
- documents) and metadata.
+ <slides file="kick-off/KM2002GO.ps" format="PS">
+ about the "Usability of MBase for MOWGLI"
+ </slides>
+ <slides file="kick-off/KM2002GO_mathweb.ps" format="PS"/>
+ <description>
+ Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
+ (to encode mathematical documents) and/or MBase (to distribute mathematical
+ documents) and metadata.
+ </description>
</presentation>
<entry author="aei/wegner">
Whenever someone is going to make a talk, he must report this to him.
projects / helm.git / blobdiff