X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmowgli%2Fhome%2Fxml%2Fslides%2Fmowgligroup.xml;fp=helm%2Fmowgli%2Fhome%2Fxml%2Fslides%2Fmowgligroup.xml;h=0000000000000000000000000000000000000000;hp=49889481e4210c339f2fca6c20b3411bdcfb143e;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff
diff --git a/helm/mowgli/home/xml/slides/mowgligroup.xml b/helm/mowgli/home/xml/slides/mowgligroup.xml
deleted file mode 100644
index 49889481e..000000000
--- a/helm/mowgli/home/xml/slides/mowgligroup.xml
+++ /dev/null
@@ -1,87 +0,0 @@
-
-
-
-
- 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.
-
-
-