+++ /dev/null
-<?xml version="1.0"?>
-
-<!DOCTYPE minutes [
- <!ELEMENT minutes (about,participant*,presentation*,entry*)>
-
- <!ELEMENT about (#PCDATA)>
-
- <!ELEMENT entry (#PCDATA)>
- <!ATTLIST entry
- author CDATA #IMPLIED>
-
- <!ELEMENT presentation (slides*,description)>
- <!ATTLIST presentation
- media (blackboard|slides) #REQUIRED
- 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
- file CDATA #REQUIRED>
-
- <!ELEMENT ul (li*)>
-
- <!ELEMENT li (#PCDATA|ul)*>
-]>
-
-<minutes>
- <about>the Kick-Off</about>
- <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>
- <entry author="aei/wegner">
- Whenever someone is going to make a talk, he must report this to him.
- </entry>
- <entry>
- To reach an agreement on the consortium agreement, Trusted Logic will
- send a completely filled-in, light version of the agreement to everybody.
- If the agreement will not satisfy everybody up to minor modifications,
- we will go for the heavy proposal.
- </entry>
- <entry author="nijmegen/geuvers">
- The members of the PCC are responsible to communicate the name of the
- site responsible for every WP.
- </entry>
- <entry>
- There will be two mailing lists. The first one (for everybody) is
- the one already created. The second one will be an administrative
- mailing list.
- </entry>
- <entry>
- All the meetings have already been scheduled: the first one will be held
- in Nijmegen from the 17th to the 19th of July. The others will be
- in Bertinoro (just after MKM03), Sophia (October 2003), Saarbrucken
- and Paris.
- </entry>
- <entry author="trusted-logic/gimenez">
- It will be simpler to have PCC meetings by phones.
- </entry>
- <entry author="aei/wegner">
- During the plenary meetings, sub-meetings will be organized to discuss
- technical details.
- </entry>
- <entry author="bologna/asperti">
- Every Package Leader must submit a contribution to the deliverable 0.a.
- </entry>
- <entry author="aei/wegner">
- It is better to use a task-force of external experts to comment on
- deliverable 1.a.
- </entry>
- <entry author="aei/wegner">
- The set of requirements must be ordered by importance (useful if some of
- them are not fulfilled).
- </entry>
- <entry>
- A long discussion on the topic of deliverable 1.c showed that there is
- some mismatch in the vocabulary of the participants.
- </entry>
- <entry author="bologna/asperti">
- The choice between MathML and OpenMath is quite difficult, because
- there are really no strong pro and cons in favor or against any of them.
- </entry>
- <entry author="aei/schutz">
- Maybe not having browsers supporting MathML is not a huge problem.
- </entry>
-</minutes>
projects / helm.git / blobdiff