helm/mowgli/home/xml/members/kick-off.xml

   1 <?xml version="1.0"?>
   2
   3 <!DOCTYPE minutes [
   4  <!ELEMENT minutes (about,participant*,presentation*,entry*)>
   5
   6  <!ELEMENT about (#PCDATA)>
   7
   8  <!ELEMENT entry (#PCDATA)>
   9  <!ATTLIST entry
  10            author CDATA #IMPLIED>
  11
  12  <!ELEMENT presentation (slides*,description)>
  13  <!ATTLIST presentation
  14            media (blackboard|slides) #REQUIRED
  15            site CDATA #REQUIRED
  16            author CDATA #REQUIRED>
  17
  18  <!ELEMENT description (#PCDATA|ul)*>
  19
  20  <!ELEMENT slides (#PCDATA)>
  21  <!ATTLIST slides
  22            file   CDATA #REQUIRED
  23            format (PowerPoint|PS|PDF|HTML) #REQUIRED>
  24
  25  <!ELEMENT participant (#PCDATA)>
  26  <!ATTLIST participant
  27            site CDATA #REQUIRED
  28            file CDATA #REQUIRED>
  29
  30  <!ELEMENT ul (li*)>
  31
  32  <!ELEMENT li (#PCDATA|ul)*>
  33 ]>
  34
  35 <minutes>
  36  <about>the Kick-Off</about>
  37  <participant site="bologna" file="asperti"/>
  38  <participant site="bologna" file="sacerdoti"/>
  39  <participant site="inria" file="herbelin"/>
  40  <participant site="inria" file="rideau"/>
  41  <participant site="inria" file="pottier"/>
  42  <participant site="inria" file="werner"/>
  43  <participant site="nijmegen" file="geuvers"/>
  44  <participant site="nijmegen" file="wiedijk"/>
  45  <participant site="dfki" file="moschner"/>
  46  <participant site="trusted-logic" file="gimenez"/>
  47  <participant site="aei" file="schutz"/>
  48  <participant site="aei" file="wegner"/>
  49  <participant site="aei" file="velden"/>
  50  <participant site="aei" file="kelley"/>
  51  <participant site="aei" file="weyher"/>
  52  <participant site="aei" file="pollney"/>
  53  <presentation site="bologna" author="asperti" media="blackboard">
  54   <description>
  55    A comparison of the aims and approaches of HELM and OpenMath.
  56   </description>
  57  </presentation>
  58  <presentation site="inria" author="pottier" media="slides">
  59   <slides file="kick-off/lemme2.ppt" format="PowerPoint"/>
  60   <description>
  61    Presentation of the work of Sophia-Antipolis: Project Lemme;
  62    PCoq (an interface to the Coq system based on Aioli [for tree management],
  63    PPML [a sort of stylesheet language] and Figue [rendering engine]).
  64   </description>
  65  </presentation>
  66  <presentation site="inria" author="herbelin" media="slides">
  67   <slides file="kick-off/MoWGLI-LogiCal.ps" format="PS"/>
  68   <description>
  69    Presentation of the work of Rocquencourt: Coq (proof assistant) and its
  70    problems:
  71    <ul>
  72     <li>Classification of theories:
  73      <ul>
  74       <li>Actually based only on the affiliation of the author.</li>
  75       <li>We should have classifications based on subject, theme, author, etc.</li>
  76      </ul>
  77     </li>
  78     <li>Retrieving:
  79      <ul>
  80       <li>By pattern. Problem: the patterns (n &lt; m+1) and (n &lt;= m) are
  81           differents but denote the same thing.</li>
  82       <li>By isomorphisms. Problem: we can capture just a few of them.</li>
  83      </ul>
  84     </li>
  85     <li>Proof Rendering in Natural Language: still too many detailed.
  86         Views at different levels of detail can probably help.
  87     </li>
  88     <li>Modularity</li>
  89    </ul>
  90   </description>
  91  </presentation>
  92  <presentation site="nijmegen" author="geuvers" media="slides">
  93   <slides file="mowgligroup.html" format="HTML"/>
  94   <description>
  95    Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
  96    planned contributions to MOWGLI.
  97   </description>
  98  </presentation>
  99  <presentation site="aei" author="wegner" media="blackboard">
 100   <description>
 101    Presentation of the projects in which he is envolved or that he is
 102    coordinating; interest in metadata; problems related to having papers
 103    in electronic form. His main contribution will be providing links to
 104    mathematicians.
 105   </description>
 106  </presentation>
 107  <presentation site="aei" author="schutz" media="slides">
 108   <slides file="kick-off/AIP_Intro.ppt" format="PowerPoint"/>
 109   <description>
 110    Presentation of the work done at the Max Planck Institute for Gravitational
 111    Physics; presentation of Living Reviews in Relativity and expectations
 112    from MOWGLI (i.e. searching, rendering, interoperability). He points out
 113    how Living Reviews in  Relativity already provide a notion of versioning;
 114    how hyperlinks are managed (often opening pop-ups). He finally presents
 115    some data that show that on-line browsing of papers really happens.
 116   </description>
 117  </presentation>
 118  <presentation site="trusted-logic" author="gimenez" media="blackboard">
 119   <description>
 120    Presentation of the work done at Trusted Logic. Brief introduction to
 121    the Common Criteria Software: lot of documentation must be produced for
 122    third (and fourth!) parties evaluation; formal evaluation is one goal
 123    (not yet reached). The main problems Trusted Logic meets are:
 124    <ul>
 125     <li>Presentation</li>
 126     <li>Managing thousands of definitions/theorems and links between them</li>
 127     <li>Evaluators needs: hiding/displaying information; different views on the
 128         same proofs/definitions; metadata; backpointers (which lemmas are
 129         used in a theorem)</li>
 130     <li>Interoperability with other software tools</li>
 131     <li>Proofs mantainance</li>
 132    </ul>
 133    A final remark is that Trusted Logic is just interested in provability
 134    (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
 135    language description of them).
 136   </description>
 137  </presentation>
 138  <presentation site="dfki" author="moschner" media="slides">
 139   <slides file="kick-off/KM2002GO.ps" format="PS">
 140    about the "Usability of MBase for MOWGLI"
 141   </slides>
 142   <slides file="kick-off/KM2002GO_mathweb.ps" format="PS"/>
 143   <description>
 144    Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
 145    (to encode mathematical documents) and/or MBase (to distribute mathematical
 146    documents) and metadata.
 147   </description>
 148  </presentation>
 149  <entry author="aei/wegner">
 150   Whenever someone is going to make a talk, he must report this to him.
 151  </entry>
 152  <entry>
 153   To reach an agreement on the consortium agreement, Trusted Logic will
 154   send a completely filled-in, light version of the agreement to everybody.
 155   If the agreement will not satisfy everybody up to minor modifications,
 156   we will go for the heavy proposal.
 157  </entry>
 158  <entry author="nijmegen/geuvers">
 159   The members of the PCC are responsible to communicate the name of the
 160   site responsible for every WP.
 161  </entry>
 162  <entry>
 163   There will be two mailing lists. The first one (for everybody) is
 164   the one already created. The second one will be an administrative
 165   mailing list.
 166  </entry>
 167  <entry>
 168   All the meetings have already been scheduled: the first one will be held
 169   in Nijmegen from the 17th to the 19th of July. The others will be
 170   in Bertinoro (just after MKM03), Sophia (October 2003), Saarbrucken
 171   and Paris.
 172  </entry>
 173  <entry author="trusted-logic/gimenez">
 174   It will be simpler to have PCC meetings by phones.
 175  </entry>
 176  <entry author="aei/wegner">
 177   During the plenary meetings, sub-meetings will be organized to discuss
 178   technical details.
 179  </entry>
 180  <entry author="bologna/asperti">
 181   Every Package Leader must submit a contribution to the deliverable 0.a.
 182  </entry>
 183  <entry author="aei/wegner">
 184   It is better to use a task-force of external experts to comment on
 185   deliverable 1.a.
 186  </entry>
 187  <entry author="aei/wegner">
 188   The set of requirements must be ordered by importance (useful if some of
 189   them are not fulfilled).
 190  </entry>
 191  <entry>
 192   A long discussion on the topic of deliverable 1.c showed that there is
 193   some mismatch in the vocabulary of the participants.
 194  </entry>
 195  <entry author="bologna/asperti">
 196   The choice between MathML and OpenMath is quite difficult, because
 197   there are really no strong pro and cons in favor or against any of them.
 198  </entry>
 199  <entry author="aei/schutz">
 200   Maybe not having browsers supporting MathML is not a huge problem.
 201  </entry>
 202 </minutes>