--- /dev/null
+<?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 & 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>
projects / helm.git / blobdiff