+++ /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