<?xml version="1.0"?>
<!DOCTYPE minutes [
- <!ELEMENT minutes (about,participant*,entry*)>
+ <!ELEMENT minutes (about,participant*,presentation*,entry*)>
<!ELEMENT about (#PCDATA)>
<!ATTLIST entry
author CDATA #IMPLIED>
+ <!ELEMENT presentation (#PCDATA|ul)*>
+ <!ATTLIST presentation
+ media (blackboard|slides) #REQUIRED
+ slides CDATA #IMPLIED
+ site CDATA #REQUIRED
+ author CDATA #REQUIRED>
+
<!ELEMENT participant (#PCDATA)>
<!ATTLIST participant
- file CDATA #IMPLIED>
+ site CDATA #REQUIRED
+ file CDATA #REQUIRED>
+
+ <!ELEMENT ul (li*)>
+
+ <!ELEMENT li (#PCDATA|ul)*>
]>
<minutes>
<about>the Kick-Off</about>
- <participant file="bologna/asperti"/>
- <participant file="bologna/sacerdoti"/>
- <participant file="inria/herbelin"/>
- <participant file="inria/rideau"/>
- <participant file="inria/pottier"/>
- <participant file="inria/werner"/>
- <participant file="nijmegen/geuvers"/>
- <participant file="nijmegen/wiedijk"/>
- <participant file="dfki/moschner"/>
- <participant file="trusted-logic/gimenez"/>
- <participant file="aei/schutz"/>
- <participant file="aei/wegner"/>
- <participant file="aei/velden"/>
- <participant file="aei/kelley"/>
+ <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">
+ A comparison of the aims and approaches of HELM and OpenMath.
+ </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>
+ <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>
+ <presentation site="nijmegen" author="geuvers" media="slides">
+ Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI;
+ planned contributions to MOWGLI.
+ </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.
+ </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>
+ <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).
+ </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.
+ </presentation>
<entry author="aei/wegner">
Whenever someone is going to make a talk, he must report this to him.
</entry>
projects / helm.git / blobdiff