+ <participant site="bologna" file="asperti"/>
+ <participant site="bologna" file="sacerdoti"/>
+ <participant site="inria" file="herbelin"/>
+ <participant site="inria" file="rideau"/>
+ <participant site="inria" file="pottier"/>
+ <participant site="inria" file="werner"/>
+ <participant site="nijmegen" file="geuvers"/>
+ <participant site="nijmegen" file="wiedijk"/>
+ <participant site="dfki" file="moschner"/>
+ <participant site="trusted-logic" file="gimenez"/>
+ <participant site="aei" file="schutz"/>
+ <participant site="aei" file="wegner"/>
+ <participant site="aei" file="velden"/>
+ <participant site="aei" file="kelley"/>
+ <participant site="aei" file="weyher"/>
+ <participant site="aei" file="pollney"/>
+ <presentation site="bologna" author="asperti" media="blackboard">
+ <description>
+ A comparison of the aims and approaches of HELM and OpenMath.
+ </description>
+ </presentation>
+ <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 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">
+ <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">
+ <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 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">
+ <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">
+ <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>