From: Claudio Sacerdoti Coen Date: Wed, 20 Mar 2002 12:18:06 +0000 (+0000) Subject: * New MOWGLI members X-Git-Tag: V_0_3_0_debian_8~204 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d22de6fda5ab935ae68e106794e7f05808aaea55;p=helm.git * New MOWGLI members * New: summary of the MOWGLI kick-off on-line --- diff --git a/helm/mowgli/home/html/Makefile b/helm/mowgli/home/html/Makefile index 1cbbc9c56..304c75d31 100644 --- a/helm/mowgli/home/html/Makefile +++ b/helm/mowgli/home/html/Makefile @@ -20,9 +20,11 @@ XHTMLCONTENT = $(XSLROOT)/xhtml-content.xsl PEOPLE = \ people/aei/kelley.html \ + people/aei/pollney.html \ people/aei/schutz.html \ people/aei/velden.html \ people/aei/wegner.html \ + people/aei/weyher.html \ people/bologna/asperti.html \ people/bologna/guidi.html \ people/bologna/padovani.html \ @@ -322,6 +324,8 @@ install: $(DOCUMENTS) mkdir -p $(DESTDIR)/misc/proposal cp ../htaccess $(DESTDIR)/misc/proposal/.htaccess cp ../misc/proposal/*.* $(DESTDIR)/misc/proposal + cp -R ../misc/kick-off $(DESTDIR)/misc + cp ../htaccess $(DESTDIR)/misc/kick-off/.htaccess if [ $(FRAMES) = yes ] ; \ then \ sed s/menu\\.html/$(HTMLDESTDIRSUFFIX)\\/menu\\.html/
  • Mailing Lists
  • The Proposal
    • -
  • Minutes of the Meetings
    • +
  • Reports of the Meetings
    • @@ -56,9 +56,9 @@
    -

    Minutes of the Meetings

    +

    Reports of the Meetings

    -

    Minutes are available for the following meetings:

    +

    Reports are available for the following meetings:

    diff --git a/helm/mowgli/home/xml/members/kick-off.xml b/helm/mowgli/home/xml/members/kick-off.xml index 1772f8975..45ca1cb88 100644 --- a/helm/mowgli/home/xml/members/kick-off.xml +++ b/helm/mowgli/home/xml/members/kick-off.xml @@ -1,7 +1,7 @@ + @@ -9,27 +9,114 @@ + + + + site CDATA #REQUIRED + file CDATA #REQUIRED> + + + + ]> 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). +     + + 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. diff --git a/helm/mowgli/home/xml/people/aei/pollney.xml b/helm/mowgli/home/xml/people/aei/pollney.xml new file mode 100644 index 000000000..76a8ef15e --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/pollney.xml @@ -0,0 +1,19 @@ + + + + + + Dennis + Pollney + Dr. + pollney@aei-potsdam.mpg.de + http://www.aei.mpg.de/cgi-bin/interface/people.cgi?key=pollney +
    + Max-Planck-Institut für Gravitationsphysik, + Albert-Einstein-Institut, + Am Mühlenberg 1, + 14476 Golm +
    + +49 (331) 567-7367 + +49 (331) 567-7298 +     diff --git a/helm/mowgli/home/xml/people/aei/weyher.xml b/helm/mowgli/home/xml/people/aei/weyher.xml new file mode 100644 index 000000000..51cc00c41 --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/weyher.xml @@ -0,0 +1,18 @@ + + + + + + Christina + Weyher + weyher@aei-potsdam.mpg.de + http://www.aei.mpg.de/cgi-bin/interface/people.cgi?key=weyher +
    + Max-Planck-Institut für Gravitationsphysik, + Albert-Einstein-Institut, + Am Mühlenberg 1, + 14476 Golm +
    + +49 (331) 567-7441 + +49 (331) 567-7449 +     diff --git a/helm/mowgli/home/xml/people/index.xml b/helm/mowgli/home/xml/people/index.xml index 9348d5bf0..d665a88ff 100644 --- a/helm/mowgli/home/xml/people/index.xml +++ b/helm/mowgli/home/xml/people/index.xml @@ -51,8 +51,10 @@ + + diff --git a/helm/mowgli/home/xsl/management.xsl b/helm/mowgli/home/xsl/management.xsl new file mode 100644 index 000000000..53fd82667 --- /dev/null +++ b/helm/mowgli/home/xsl/management.xsl @@ -0,0 +1,192 @@ + + + + + + + + + + + + Project Management + + + + + + + + + + +
    + +
    + + +     + + +
    + Project Manager: + + + + + +
    +
    + +
    +     + + +
    + Exploitation Manager: + + + + + +
    +
    + +
    +     + + +
    + Work-Package Leaders +
    +
    + + + + + + + + + + + +
    + + + +
    + + + + + + +
    + +
    +     + + +
    + Technical Contributors +
    +
    + +
    +     + + +
    + Project Coordination Committee +
    +
    +

    + Chaired by + + + + + + +

    +

    + Members: + + + + + + + + + + + + +
    + + + + + + +
    +     +

    + +
    +     + + +
    + Project Exploitation Board +
    +
    +

    + Chaired by + + + + + + +

    +

    + Members: + + + + + + + + + + + + +
    + + + + + +
    +     +

    + +
    +     + + +
    + Work-Package Teams +
    +
    + +
    +     + +     diff --git a/helm/mowgli/home/xsl/minutes.xsl b/helm/mowgli/home/xsl/minutes.xsl new file mode 100644 index 000000000..e0bc462a3 --- /dev/null +++ b/helm/mowgli/home/xsl/minutes.xsl @@ -0,0 +1,101 @@ + + + + + + + + + + + + + <xsl:text>Summary of </xsl:text> + <xsl:value-of select="minutes/about"/> + + + +

    Summary of

    +

    Participants:

    +
      + + + +
    +

    Presentations:

    +
    + +
    +

    Minutes:

    +

    + Note: + The following entries reports only the important observations raised during + the meeting and the decisions taken. +

    +
      + +
    + + +     + + +
  • + + [ + + + + + + ] + + +
    • +     + + +
  • + + + + + +   ( + + ) +
    • +     + + +
    + + + + + +  ( + + ): + + + + [ + + Get the slides + + ] + + + [slides unavailable] + + + +
    +
    + +
    +     + +