]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: b1ab224)
* Slides can now also be in XHTML format
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 2 May 2002 12:52:48 +0000 (12:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 2 May 2002 12:52:48 +0000 (12:52 +0000)
* Nijmegen's slides for the kick-off added
* Rendering of the management information improved (table border)

helm/mowgli/home/html/Makefile patch | blob | history
helm/mowgli/home/html/slides/.cvsignore [new file with mode: 0644] patch | blob
helm/mowgli/home/xml/members/kick-off.xml patch | blob | history
helm/mowgli/home/xml/slides/mowgligroup.xml [new file with mode: 0644] patch | blob
helm/mowgli/home/xsl/management.xsl patch | blob | history
helm/mowgli/home/xsl/minutes.xsl patch | blob | history

diff --git a/helm/mowgli/home/html/Makefile b/helm/mowgli/home/html/Makefile
index 805650404d4b0e5f2364bc5216b3e74dec636886..dc9365a5be4ad1a0a7cc624d0b27d428575333f1 100644 (file)
--- a/helm/mowgli/home/html/Makefile
+++ b/helm/mowgli/home/html/Makefile
@@ -79,6 +79,7 @@ DOCUMENTS = \
            mowgli-events.html \
            deadlines.html \
            people-list.html \
+            slides/mowgligroup.html \
             deliverables/distribution/d5a.html \
             deliverables/distribution/d5b.html \
             deliverables/information-dissemination-and-exploitation/d7a.html \
@@ -173,6 +174,9 @@ index.html: $(TEMPLATESROOT)/index.html
 members/ml-help-example.txt: $(TEMPLATESROOT)/ml-help-example.txt
        cp $< $@
 
+slides/%.html: $(XMLROOT)/slides/%.xml $(XHTMLCONTENT)
+       $(XSLTP) --param path_to_top "'..'" --param use_frames "'$(FRAMES)'" -o $@ $(XHTMLCONTENT) $<
+
 members/index.html: $(XMLROOT)/members-index.xml \
                    $(XHTMLCONTENT)
        sed $(RMDOCTYPE) $< | $(XSLTP) --param path_to_top "'..'" --param use_frames "'$(FRAMES)'" -o $@ $(XHTMLCONTENT) -
diff --git a/helm/mowgli/home/html/slides/.cvsignore b/helm/mowgli/home/html/slides/.cvsignore
new file mode 100644 (file)
index 0000000..64a8aa4
--- /dev/null
+++ b/helm/mowgli/home/html/slides/.cvsignore
@@ -0,0 +1 @@
+mowgligroup.html
diff --git a/helm/mowgli/home/xml/members/kick-off.xml b/helm/mowgli/home/xml/members/kick-off.xml
index 5fd4d3e430a8edd1de82dd635c7f49a91cd7ffb5..2b8028f01ad94abf3348bc821835ff4b61415782 100644 (file)
--- a/helm/mowgli/home/xml/members/kick-off.xml
+++ b/helm/mowgli/home/xml/members/kick-off.xml
@@ -20,7 +20,7 @@
  <!ELEMENT slides (#PCDATA)>
  <!ATTLIST slides
            file   CDATA #REQUIRED
-           format (PowerPoint|PS|PDF) #REQUIRED>
+           format (PowerPoint|PS|PDF|HTML) #REQUIRED>
 
  <!ELEMENT participant (#PCDATA)>
  <!ATTLIST participant
@@ -90,6 +90,7 @@
   </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.
diff --git a/helm/mowgli/home/xml/slides/mowgligroup.xml b/helm/mowgli/home/xml/slides/mowgligroup.xml
new file mode 100644 (file)
index 0000000..4988948
--- /dev/null
+++ b/helm/mowgli/home/xml/slides/mowgligroup.xml
@@ -0,0 +1,87 @@
+<?xml version="1.0"?>
+
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+ <title>Activities in the Nijmegen - Eindhoven site</title>
+</head>
+<body>
+<H1> MOWGLI Kick-Off Meeting Berlin, March 15, 2002</H1>
+
+<H3>Activities in the Nijmegen - Eindhoven site</H3>
+
+
+<H4>People</H4>
+<B> Nijmegen</B>:
+<UL>
+<LI> Henk Barendregt (prof.) </LI>
+<LI>  Herman Geuvers (assoc. prof.) </LI>
+<LI>  Freek Wiedijk (post-doc)  </LI>
+<LI>  Dan Synek (sci. progr.) </LI>
+<LI>  Milad Niqui (Ph.D. stud.) </LI>
+<LI>  Jasper Stein (Ph.D. stud.) </LI>
+<LI>  Luis Cruz-Filipe (Ph.D. stud.) </LI>
+<LI>  Georgi Jojgov (Ph.D. stud.) </LI>
+</UL>
+<B> Eindhoven</B>
+<UL>
+<LI> Arjeh Cohen (prof.) </LI>
+<LI> Scott Murray (post-doc) </LI>
+<LI> Ernesto Reinaldo (Ph.D. stud.) </LI>
+</UL>
+<H4>Focus</H4>
+<B> Nijmegen</B>:
+<B>Formalizing Mathematics</B>: To devise and study computer systems
+for formalizing mathematics, which includes mathematical activities as
+defining, computing and proving, but also the
+activities of presenting and editing formalized
+mathematics.
+<BR />
+<B> Eindhoven</B>
+<B>Interactive Mathematical Documents</B>: Mathematical documents on
+the WWW, with interaction possibilities with various
+mathematical applications. Use of OpenMath (resp.
+OmDoc) to represent these documents, in order to have
+semantically meaningful representation of mathematical objects.
+
+<H4> Actual Activities</H4>
+<UL>
+<LI> Study the underlying formal logic of theorem provers. </LI>
+<LI> Formalizing mathematics (Coq: FTA, Analysis, Lin.
+Alg., Reals). </LI>
+<LI> Adding automation/computation facilities to a theorem
+prover (Coq). </LI>
+<LI> Investigate various proof styles, notably by comparing
+various theorem provers (Coq, Mizar, Hol-light). </LI>
+<LI> Develop a benchmark for mathematical theorem provers. </LI>
+<LI> Study the presentation and communication of proof developments. </LI>
+<LI> Development and use of OpenMath as a language for coding
+and communicating `meaningful' mathematical objects. </LI>
+<LI> IDA: Interactive Course Notes Algebra, based on OpenMath/OMDoc. </LI>
+<LI> Develop packages for XML-based interaction between
+math. applications. </LI>
+</UL>
+
+<H4> Interest in Mowgli</H4>
+<UL> 
+<LI> Rendering of Libraries of Formalized Mathematics. </LI>
+<LI> Searching/Retrieving information (knowledge) from these Libraries. </LI>
+<LI> Presentation of Formal proof/theory developments. </LI>
+</UL>
+
+<H4> Interest in Mowgli</H4>
+<UL> 
+<LI> Rendering of Libraries of Formalized Mathematics. </LI>
+<LI> Searching/Retrieving information (knowledge) from these Libraries. </LI>
+<LI> Presentation of Formal proof/theory developments. </LI>
+</UL>
+
+
+<H4> Planned Contribution to Mowgli</H4>
+<UL> 
+<LI> Requirements Analysis: What do we need &amp; What is already there? </LI>
+<LI> Transformation of formal proofs (into MathMl/XML/...). </LI>
+<LI> Generation of Natural Language proofs. (Views on proofs.) </LI>
+<LI> Validation of the system through large math. theory developments. </LI>
+</UL>
+</body>
+</html>
diff --git a/helm/mowgli/home/xsl/management.xsl b/helm/mowgli/home/xsl/management.xsl
index 15708594177cb3bd01abb24d8315cf9de76ca7b3..a0fb276cc74879a5fa68fcc62fc2bcbdab549127 100644 (file)
--- a/helm/mowgli/home/xsl/management.xsl
+++ b/helm/mowgli/home/xsl/management.xsl
@@ -61,7 +61,7 @@
   <span style="font-weight: bold">Work-Package Leaders</span>
  </dt>
  <dd>
-  <table>
+  <table border="1">
    <tr>
     <xsl:for-each select="document('../xml/work-packages/index.xml')/work-packages/work-package">
      <td>
@@ -114,7 +114,7 @@
   <p>
    <xsl:text>Members:</xsl:text>
    <span style="margin-left: 1cm">
-    <table>
+    <table border="1">
      <tr>
       <xsl:for-each select="member">
        <td style="text-align: center">
@@ -160,7 +160,7 @@
   <p>
    <xsl:text>Members:</xsl:text>
    <span style="margin-left: 1cm">
-    <table>
+    <table border="1">
      <tr>
       <xsl:for-each select="member">
        <td style="text-align: center">
diff --git a/helm/mowgli/home/xsl/minutes.xsl b/helm/mowgli/home/xsl/minutes.xsl
index 26a01e014df0e5de58c31412f538a75f19eae83f..0270a159d9fe72aa14a58885a2fad184ff1f4c69 100644 (file)
--- a/helm/mowgli/home/xsl/minutes.xsl
+++ b/helm/mowgli/home/xsl/minutes.xsl
@@ -87,7 +87,17 @@
     <xsl:when test="slides">
      <xsl:for-each select="slides">
       <xsl:text>[</xsl:text>
-      <a href="../../misc/{@file}">
+      <xsl:variable name="location">
+       <xsl:choose>
+        <xsl:when test="@format = 'HTML'">
+         <xsl:value-of select="concat('../slides/',@file)"/>
+        </xsl:when>
+        <xsl:otherwise>
+         <xsl:value-of select="concat('../../misc/',@file)"/>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:variable>
+      <a href="{$location}">
        <xsl:text>Get the slides</xsl:text>
        <xsl:if test="text()">
         <xsl:text> </xsl:text>
Unnamed repository; edit this file 'description' to name the repository.