X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fmembers%2Fkick-off.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fmembers%2Fkick-off.xml;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=2b8028f01ad94abf3348bc821835ff4b61415782;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/mowgli/home/xml/members/kick-off.xml b/helm/mowgli/home/xml/members/kick-off.xml deleted file mode 100644 index 2b8028f01..000000000 --- a/helm/mowgli/home/xml/members/kick-off.xml +++ /dev/null @@ -1,202 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - -]> - - - the Kick-Off - - - - - - - - - - - - - - - - - - - A comparison of the aims and approaches of HELM and OpenMath. - - - - - - 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 of the work of Rocquencourt: Coq (proof assistant) and its - problems: -
    -
  • Classification of theories: -
      -
    • Actually based only on the affiliation of the author.
      • -
    • We should have classifications based on subject, theme, author, etc.
      • -
    -
    • -
  • Retrieving: -
      -
    • By pattern. Problem: the patterns (n < m+1) and (n <= m) are - differents but denote the same thing.
      • -
    • By isomorphisms. Problem: we can capture just a few of them.
      • -
    -
    • -
  • Proof Rendering in Natural Language: still too many detailed. - Views at different levels of detail can probably help. -
    • -
  • Modularity
    • -
- - - - - - Presentation of the work of Nijmegen; why Nijmegen is interested in MOWGLI; - planned contributions to MOWGLI. - - - - - 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 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 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: -
    -
  • Presentation
    • -
  • Managing thousands of definitions/theorems and links between them
    • -
  • Evaluators needs: hiding/displaying information; different views on the - same proofs/definitions; metadata; backpointers (which lemmas are - used in a theorem)
    • -
  • Interoperability with other software tools
    • -
  • Proofs mantainance
    • -
- 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). - - - - - about the "Usability of MBase for MOWGLI" - - - - Presentation of the work done at DFKI. Contributions to MOWGLI: OMDoc - (to encode mathematical documents) and/or MBase (to distribute mathematical - documents) and metadata. - - - - Whenever someone is going to make a talk, he must report this to him. - - - 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. - - - The members of the PCC are responsible to communicate the name of the - site responsible for every WP. - - - 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. - - - 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. - - - It will be simpler to have PCC meetings by phones. - - - During the plenary meetings, sub-meetings will be organized to discuss - technical details. - - - Every Package Leader must submit a contribution to the deliverable 0.a. - - - It is better to use a task-force of external experts to comment on - deliverable 1.a. - - - The set of requirements must be ordered by importance (useful if some of - them are not fulfilled). - - - A long discussion on the topic of deliverable 1.c showed that there is - some mismatch in the vocabulary of the participants. - - - 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. - - - Maybe not having browsers supporting MathML is not a huge problem. - -