From 9fcfeb79982284413f5a3f6d375ee0bad5368d9c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 May 2002 12:52:48 +0000 Subject: [PATCH] * Slides can now also be in XHTML format * Nijmegen's slides for the kick-off added * Rendering of the management information improved (table border) --- helm/mowgli/home/html/Makefile | 4 + helm/mowgli/home/html/slides/.cvsignore | 1 + helm/mowgli/home/xml/members/kick-off.xml | 3 +- helm/mowgli/home/xml/slides/mowgligroup.xml | 87 +++++++++++++++++++++ helm/mowgli/home/xsl/management.xsl | 6 +- helm/mowgli/home/xsl/minutes.xsl | 12 ++- 6 files changed, 108 insertions(+), 5 deletions(-) create mode 100644 helm/mowgli/home/html/slides/.cvsignore create mode 100644 helm/mowgli/home/xml/slides/mowgligroup.xml diff --git a/helm/mowgli/home/html/Makefile b/helm/mowgli/home/html/Makefile index 805650404..dc9365a5b 100644 --- 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 index 000000000..64a8aa4e0 --- /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 5fd4d3e43..2b8028f01 100644 --- a/helm/mowgli/home/xml/members/kick-off.xml +++ b/helm/mowgli/home/xml/members/kick-off.xml @@ -20,7 +20,7 @@ + format (PowerPoint|PS|PDF|HTML) #REQUIRED> + 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 index 000000000..49889481e --- /dev/null +++ b/helm/mowgli/home/xml/slides/mowgligroup.xml @@ -0,0 +1,87 @@ + + + + + Activities in the Nijmegen - Eindhoven site + + +

MOWGLI Kick-Off Meeting Berlin, March 15, 2002

+ +

Activities in the Nijmegen - Eindhoven site

+ + +

People

+ Nijmegen: +
    +
  • Henk Barendregt (prof.)
    • +
  • Herman Geuvers (assoc. prof.)
    • +
  • Freek Wiedijk (post-doc)
    • +
  • Dan Synek (sci. progr.)
    • +
  • Milad Niqui (Ph.D. stud.)
    • +
  • Jasper Stein (Ph.D. stud.)
    • +
  • Luis Cruz-Filipe (Ph.D. stud.)
    • +
  • Georgi Jojgov (Ph.D. stud.)
    • +
+ Eindhoven +
    +
  • Arjeh Cohen (prof.)
    • +
  • Scott Murray (post-doc)
    • +
  • Ernesto Reinaldo (Ph.D. stud.)
    • +
+

Focus

+ Nijmegen: +Formalizing Mathematics: 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. +
+ Eindhoven +Interactive Mathematical Documents: 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. + +

Actual Activities

+
    +
  • Study the underlying formal logic of theorem provers.
    • +
  • Formalizing mathematics (Coq: FTA, Analysis, Lin. +Alg., Reals).
    • +
  • Adding automation/computation facilities to a theorem +prover (Coq).
    • +
  • Investigate various proof styles, notably by comparing +various theorem provers (Coq, Mizar, Hol-light).
    • +
  • Develop a benchmark for mathematical theorem provers.
    • +
  • Study the presentation and communication of proof developments.
    • +
  • Development and use of OpenMath as a language for coding +and communicating `meaningful' mathematical objects.
    • +
  • IDA: Interactive Course Notes Algebra, based on OpenMath/OMDoc.
    • +
  • Develop packages for XML-based interaction between +math. applications.
    • +
+ +

Interest in Mowgli

+
    +
  • Rendering of Libraries of Formalized Mathematics.
    • +
  • Searching/Retrieving information (knowledge) from these Libraries.
    • +
  • Presentation of Formal proof/theory developments.
    • +
+ +

Interest in Mowgli

+
    +
  • Rendering of Libraries of Formalized Mathematics.
    • +
  • Searching/Retrieving information (knowledge) from these Libraries.
    • +
  • Presentation of Formal proof/theory developments.
    • +
+ + +

Planned Contribution to Mowgli

+
    +
  • Requirements Analysis: What do we need & What is already there?
    • +
  • Transformation of formal proofs (into MathMl/XML/...).
    • +
  • Generation of Natural Language proofs. (Views on proofs.)
    • +
  • Validation of the system through large math. theory developments.
    • +
+ + diff --git a/helm/mowgli/home/xsl/management.xsl b/helm/mowgli/home/xsl/management.xsl index 157085941..a0fb276cc 100644 --- a/helm/mowgli/home/xsl/management.xsl +++ b/helm/mowgli/home/xsl/management.xsl @@ -61,7 +61,7 @@ Work-Package Leaders
- +
@@ -114,7 +114,7 @@

Members: - +
@@ -160,7 +160,7 @@

Members: - +
diff --git a/helm/mowgli/home/xsl/minutes.xsl b/helm/mowgli/home/xsl/minutes.xsl index 26a01e014..0270a159d 100644 --- a/helm/mowgli/home/xsl/minutes.xsl +++ b/helm/mowgli/home/xsl/minutes.xsl @@ -87,7 +87,17 @@ [ - + + + + + + + + + + + Get the slides -- 2.39.2