4 <!ELEMENT minutes (about,participant*,presentation*,entry*)>
6 <!ELEMENT about (#PCDATA)>
8 <!ELEMENT entry (#PCDATA)>
10 author CDATA #IMPLIED>
12 <!ELEMENT presentation (slides*,description)>
13 <!ATTLIST presentation
14 media (blackboard|slides) #REQUIRED
16 author CDATA #REQUIRED>
18 <!ELEMENT description (#PCDATA|ul)*>
20 <!ELEMENT slides (#PCDATA)>
23 format (PowerPoint|PS|PDF) #REQUIRED>
25 <!ELEMENT participant (#PCDATA)>
32 <!ELEMENT li (#PCDATA|ul)*>
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">
55 A comparison of the aims and approaches of HELM and OpenMath.
58 <presentation site="inria" author="pottier" media="slides">
59 <slides file="kick-off/lemme2.ppt" format="PowerPoint"/>
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]).
66 <presentation site="inria" author="herbelin" media="slides">
67 <slides file="kick-off/MoWGLI-LogiCal.ps" format="PS"/>
69 Presentation of the work of Rocquencourt: Coq (proof assistant) and its
72 <li>Classification of theories:
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>
80 <li>By pattern. Problem: the patterns (n < m+1) and (n <= m) are
81 differents but denote the same thing.</li>
82 <li>By isomorphisms. Problem: we can capture just a few of them.</li>
85 <li>Proof Rendering in Natural Language: still too many detailed.
86 Views at different levels of detail can probably help.
92 <presentation site="nijmegen" author="geuvers" media="slides">
94 Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
95 planned contributions to MOWGLI.
98 <presentation site="aei" author="wegner" media="blackboard">
100 Presentation of the projects in which he is envolved or that he is
101 coordinating; interest in metadata; problems related to having papers
102 in electronic form. His main contribution will be providing links to
106 <presentation site="aei" author="schutz" media="slides">
107 <slides file="kick-off/AIP_Intro.ppt" format="PowerPoint"/>
109 Presentation of the work done at the Max Planck Institute for Gravitational
110 Physics; presentation of Living Reviews in Relativity and expectations
111 from MOWGLI (i.e. searching, rendering, interoperability). He points out
112 how Living Reviews in Relativity already provide a notion of versioning;
113 how hyperlinks are managed (often opening pop-ups). He finally presents
114 some data that show that on-line browsing of papers really happens.
117 <presentation site="trusted-logic" author="gimenez" media="blackboard">
119 Presentation of the work done at Trusted Logic. Brief introduction to
120 the Common Criteria Software: lot of documentation must be produced for
121 third (and fourth!) parties evaluation; formal evaluation is one goal
122 (not yet reached). The main problems Trusted Logic meets are:
124 <li>Presentation</li>
125 <li>Managing thousands of definitions/theorems and links between them</li>
126 <li>Evaluators needs: hiding/displaying information; different views on the
127 same proofs/definitions; metadata; backpointers (which lemmas are
128 used in a theorem)</li>
129 <li>Interoperability with other software tools</li>
130 <li>Proofs mantainance</li>
132 A final remark is that Trusted Logic is just interested in provability
133 (and proof-scripts) and not in proofs (i.e. lambda-terms or natural
134 language description of them).
137 <presentation site="dfki" author="moschner" media="slides">
138 <slides file="kick-off/KM2002GO.ps" format="PS">
139 about the "Usability of MBase for MOWGLI"
141 <slides file="kick-off/KM2002GO_mathweb.ps" format="PS"/>
143 Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc
144 (to encode mathematical documents) and/or MBase (to distribute mathematical
145 documents) and metadata.
148 <entry author="aei/wegner">
149 Whenever someone is going to make a talk, he must report this to him.
152 To reach an agreement on the consortium agreement, Trusted Logic will
153 send a completely filled-in, light version of the agreement to everybody.
154 If the agreement will not satisfy everybody up to minor modifications,
155 we will go for the heavy proposal.
157 <entry author="nijmegen/geuvers">
158 The members of the PCC are responsible to communicate the name of the
159 site responsible for every WP.
162 There will be two mailing lists. The first one (for everybody) is
163 the one already created. The second one will be an administrative
167 All the meetings have already been scheduled: the first one will be held
168 in Nijmegen from the 17th to the 19th of July. The others will be
169 in Bertinoro (just after MKM03), Sophia (October 2003), Saarbrucken
172 <entry author="trusted-logic/gimenez">
173 It will be simpler to have PCC meetings by phones.
175 <entry author="aei/wegner">
176 During the plenary meetings, sub-meetings will be organized to discuss
179 <entry author="bologna/asperti">
180 Every Package Leader must submit a contribution to the deliverable 0.a.
182 <entry author="aei/wegner">
183 It is better to use a task-force of external experts to comment on
186 <entry author="aei/wegner">
187 The set of requirements must be ordered by importance (useful if some of
188 them are not fulfilled).
191 A long discussion on the topic of deliverable 1.c showed that there is
192 some mismatch in the vocabulary of the participants.
194 <entry author="bologna/asperti">
195 The choice between MathML and OpenMath is quite difficult, because
196 there are really no strong pro and cons in favor or against any of them.
198 <entry author="aei/schutz">
199 Maybe not having browsers supporting MathML is not a huge problem.