helm/mowgli/home/xml/slides/mowgligroup.xml

   1 <?xml version="1.0"?>
   2
   3 <html xmlns="http://www.w3.org/1999/xhtml">
   4 <head>
   5  <title>Activities in the Nijmegen - Eindhoven site</title>
   6 </head>
   7 <body>
   8 <H1> MOWGLI Kick-Off Meeting Berlin, March 15, 2002</H1>
   9
  10 <H3>Activities in the Nijmegen - Eindhoven site</H3>
  11
  12
  13 <H4>People</H4>
  14 <B> Nijmegen</B>:
  15 <UL>
  16 <LI> Henk Barendregt (prof.) </LI>
  17 <LI>  Herman Geuvers (assoc. prof.) </LI>
  18 <LI>  Freek Wiedijk (post-doc)  </LI>
  19 <LI>  Dan Synek (sci. progr.) </LI>
  20 <LI>  Milad Niqui (Ph.D. stud.) </LI>
  21 <LI>  Jasper Stein (Ph.D. stud.) </LI>
  22 <LI>  Luis Cruz-Filipe (Ph.D. stud.) </LI>
  23 <LI>  Georgi Jojgov (Ph.D. stud.) </LI>
  24 </UL>
  25 <B> Eindhoven</B>
  26 <UL>
  27 <LI> Arjeh Cohen (prof.) </LI>
  28 <LI> Scott Murray (post-doc) </LI>
  29 <LI> Ernesto Reinaldo (Ph.D. stud.) </LI>
  30 </UL>
  31 <H4>Focus</H4>
  32 <B> Nijmegen</B>:
  33 <B>Formalizing Mathematics</B>: To devise and study computer systems
  34 for formalizing mathematics, which includes mathematical activities as
  35 defining, computing and proving, but also the
  36 activities of presenting and editing formalized
  37 mathematics.
  38 <BR />
  39 <B> Eindhoven</B>
  40 <B>Interactive Mathematical Documents</B>: Mathematical documents on
  41 the WWW, with interaction possibilities with various
  42 mathematical applications. Use of OpenMath (resp.
  43 OmDoc) to represent these documents, in order to have
  44 semantically meaningful representation of mathematical objects.
  45
  46 <H4> Actual Activities</H4>
  47 <UL>
  48 <LI> Study the underlying formal logic of theorem provers. </LI>
  49 <LI> Formalizing mathematics (Coq: FTA, Analysis, Lin.
  50 Alg., Reals). </LI>
  51 <LI> Adding automation/computation facilities to a theorem
  52 prover (Coq). </LI>
  53 <LI> Investigate various proof styles, notably by comparing
  54 various theorem provers (Coq, Mizar, Hol-light). </LI>
  55 <LI> Develop a benchmark for mathematical theorem provers. </LI>
  56 <LI> Study the presentation and communication of proof developments. </LI>
  57 <LI> Development and use of OpenMath as a language for coding
  58 and communicating `meaningful' mathematical objects. </LI>
  59 <LI> IDA: Interactive Course Notes Algebra, based on OpenMath/OMDoc. </LI>
  60 <LI> Develop packages for XML-based interaction between
  61 math. applications. </LI>
  62 </UL>
  63
  64 <H4> Interest in Mowgli</H4>
  65 <UL>
  66 <LI> Rendering of Libraries of Formalized Mathematics. </LI>
  67 <LI> Searching/Retrieving information (knowledge) from these Libraries. </LI>
  68 <LI> Presentation of Formal proof/theory developments. </LI>
  69 </UL>
  70
  71 <H4> Interest in Mowgli</H4>
  72 <UL>
  73 <LI> Rendering of Libraries of Formalized Mathematics. </LI>
  74 <LI> Searching/Retrieving information (knowledge) from these Libraries. </LI>
  75 <LI> Presentation of Formal proof/theory developments. </LI>
  76 </UL>
  77
  78
  79 <H4> Planned Contribution to Mowgli</H4>
  80 <UL>
  81 <LI> Requirements Analysis: What do we need &amp; What is already there? </LI>
  82 <LI> Transformation of formal proofs (into MathMl/XML/...). </LI>
  83 <LI> Generation of Natural Language proofs. (Views on proofs.) </LI>
  84 <LI> Validation of the system through large math. theory developments. </LI>
  85 </UL>
  86 </body>
  87 </html>