From: Claudio Sacerdoti Coen Date: Tue, 12 Feb 2002 18:11:02 +0000 (+0000) Subject: Initial commit of the XML/XSLT stuff. X-Git-Tag: V_0_3_0_debian_8~343 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8ad1d26122af00feda930086b6cfa42de0139fe;p=helm.git Initial commit of the XML/XSLT stuff. The generated HTML files are not integrated with the rest of the site, yet. --- diff --git a/helm/mowgli/home/html/Makefile b/helm/mowgli/home/html/Makefile new file mode 100644 index 000000000..0d514f07d --- /dev/null +++ b/helm/mowgli/home/html/Makefile @@ -0,0 +1,104 @@ +TEMPLATESROOT = ../templates +XMLROOT = ../xml +XSLROOT = ../xsl +DOCUMENTS = home.html index.html menu.html \ + consortium.html \ + project.html \ + sites/aei.html \ + sites/bologna.html \ + sites/dfki.html \ + sites/inria.html \ + sites/nijmegen.html \ + sites/trusted-logic.html \ + people/aei/kelley.html \ + people/aei/schutz.html \ + people/aei/velden.html \ + people/aei/wegner.html \ + people/bologna/asperti.html \ + people/bologna/guidi.html \ + people/bologna/padovani.html \ + people/bologna/sacerdoti.html \ + people/bologna/schena.html \ + people/dfki/kohlhase.html \ + people/dfki/melis.html \ + people/dfki/siekmann.html \ + people/inria/amerkad.html \ + people/inria/bertot.html \ + people/inria/chicli.html \ + people/inria/delahaye.html \ + people/inria/herbelin.html \ + people/inria/naciri.html \ + people/inria/pottier.html \ + people/inria/rideau.html \ + people/inria/thery.html \ + people/nijmegen/barendregt.html \ + people/nijmegen/barreiro.html \ + people/nijmegen/cohen.html \ + people/nijmegen/cruz-filipe.html \ + people/nijmegen/geuvers.html \ + people/nijmegen/niqui.html \ + people/nijmegen/stein.html \ + people/nijmegen/synek.html \ + people/nijmegen/wiedijk.html \ + people/trusted-logic/bolignano.html \ + publications/others/category_al.html \ + publications/others/crimea2001_apss.html \ + publications/others/cup_s.html \ + publications/others/cup_s2.html \ + publications/others/extreme2001_apss.html \ + publications/others/har_bg.html \ + publications/others/jep_ws.html \ + publications/others/jep_wwsw.html \ + publications/others/jlp2001_scg.html \ + publications/others/mathml2000_apss.html \ + publications/others/mscs_gb.html \ + publications/others/tcs2001_og.html \ + publications/others/tphols2000_gwz.html \ + publications/others/tphols2001_apss.html \ + work-packages/distribution.html \ + work-packages/information-dissemination-and-exploitation.html \ + work-packages/interfaces.html \ + work-packages/metadata.html \ + work-packages/project-management.html \ + work-packages/requirement-analysis.html \ + work-packages/testing-and-validation.html \ + work-packages/transformation.html + +all: $(DOCUMENTS) + +home.html: $(TEMPLATESROOT)/home.html + cp $(TEMPLATESROOT)/home.html . + +index.html: $(TEMPLATESROOT)/index.html + cp $(TEMPLATESROOT)/index.html . + +menu.html: $(TEMPLATESROOT)/menu.html + cp $(TEMPLATESROOT)/menu.html . + +consortium.html: $(XMLROOT)/consortium.xml \ + $(XSLROOT)/consortium.xsl + xsltproc -o $@ $(XSLROOT)/consortium.xsl $(XMLROOT)/consortium.xml + +project.html: $(XMLROOT)/project.xml \ + $(XSLROOT)/project.xsl + xsltproc -o $@ $(XSLROOT)/project.xsl $(XMLROOT)/project.xml + +sites/%.html: $(XMLROOT)/$(@:%.html=%.xml) \ + $(XSLROOT)/site.xsl + xsltproc -o $@ $(XSLROOT)/site.xsl $(XMLROOT)/$(@:%.html=%.xml) + +people/%.html: $(XMLROOT)/$(@:%.html=%.xml) \ + $(XSLROOT)/person.xsl + xsltproc -o $@ $(XSLROOT)/person.xsl $(XMLROOT)/$(@:%.html=%.xml) + +publications/%.html: $(XMLROOT)/$(@:%.html=%.xml) \ + $(XSLROOT)/publication.xsl + xsltproc -o $@ $(XSLROOT)/publication.xsl $(XMLROOT)/$(@:%.html=%.xml) + +work-packages/%.html: $(XMLROOT)/$(@:%.html=%.xml) \ + $(XSLROOT)/work-package.xsl + xsltproc -o $@ $(XSLROOT)/work-package.xsl $(XMLROOT)/$(@:%.html=%.xml) + +clean: + rm -f $(DOCUMENTS) +.PHONY: clean diff --git a/helm/mowgli/home/templates/home.html b/helm/mowgli/home/templates/home.html index c824034e9..7edfbb24a 100644 --- a/helm/mowgli/home/templates/home.html +++ b/helm/mowgli/home/templates/home.html @@ -6,13 +6,13 @@ MoWGLI Home Page - +

- +
diff --git a/helm/mowgli/home/templates/menu.html b/helm/mowgli/home/templates/menu.html index a277996f9..894dc63e6 100644 --- a/helm/mowgli/home/templates/menu.html +++ b/helm/mowgli/home/templates/menu.html @@ -6,7 +6,7 @@ MoWGLI Menu - + diff --git a/helm/mowgli/home/xml/consortium.xml b/helm/mowgli/home/xml/consortium.xml new file mode 100644 index 000000000..99cd1bea9 --- /dev/null +++ b/helm/mowgli/home/xml/consortium.xml @@ -0,0 +1,190 @@ + + + + + + + + + + + + + + + + + +]> + + + + + + + + + +

The Consortium has been built with the aim to join some essential + knowhow in different areas of I.T. related to the creation and + maintenance of a digital library of structured mathematical knowledge.

+ +

MOWGLI is meant to develop the technological infrastructure required to + integrate existing Markup languages and standards such as + MathML, + OpenMath or + OMDoc, + covering different aspects of mathematical + intelligence, into a single application. + Expertise on these languages and the related technologies is + respectively provided by the following partners:

+
+
MathML
+
Department of Computer Science, University of Bologna, + member of the World Wide Web Consortium and of the W3C Working Group + on MathML; Lemme-Project at INRIA Sophia-Antipolis.
+ +
OpenMath
+
University of Eindhoven (sub-site of Nijmegen): + Professor Arjeh Cohen is one of the leaders of the + OpenMath initiative, and MOWGLI is expected to take the maximum profit + from the successful OpenMath Esprit project, no.24969.
+ +
OMDoc
+
DFKI. Dr.Michael Kohlhase is the main + auhtor of OMDoc; DFKI has a long research tradition in the management of + mathematical knowledge bases, metadata, searching and retrieval + issues.
+
+ +

More generally, the Department of Computer Science in Bologna has a + long experience in XML-related technology, and in particular in their + application to the particular domain of mathematical developments, + as testified by the + ``Hypertextual Electronic Library + of Mathematics'' (HELM) Project. A main + component of HELM is the + GtkMathView + widget, a C++ rendering engine for MathML that will be distributed as + an official package of the next Debian release of Linux.

+ +

Similarly, the Lemme Project in Sophia-Antipolis has a large experience of + edition of mathematical objects. It develops the graphical environment + Pcoq, dedicated to the development of mathematical proofs, using the + Coq proof assistant. Among many features, Pcoq has a sophisticated two + dimensional formula and natural language proof edition component, + allowing intuitive and powerful interactions. Built on the Figue + environment, Pcoq can be made compatible with MathML. The Pcoq interface + is intensively used by teams whose research activity concerns + the certification of mathematical algorithms.

+ +

DFKI will contribute requirements and metadata from the + viewpoint of educational applications including search + functionalities. It will actively work on presentational transformations, + the generation of proofs in natural language as well as on knowledge bases + for mathematical knowledge DFKI intends to exploit the results of the + MOWGLI project in pilot applications in current and planned research and + in projects for the prototypical implementation of intelligent + environments for learning of mathematics. In particular, the knowledge + representation for mathematics on the Web is important for such Web-based + systems. Knowledge bases that provide a common repository and ontology for + mathematical knowledge are indispensible in systems that integrate various + systems working on mathematical knowledge. DFKI also has a fierce interest + in pushing and leveraging the quality of standardisation efforts within + the worldwide initiative of the Semantic Web education systems and + electronic publishing.

+ +

In order to immediately dispose of a large repository of structured + mathematical information, the consortium comprises the developers of + one of the most successful proof assistant tools currently + available: the Coq proof + engine of INRIA-Rocquencourt. + The Coq standard library includes more than thousand lemmas and theorems + and the whole number of statements proved by users is evaluated to + hundred thousands, covering arithmetics, algebra, analysis and + computer science. We expect to integrate the current different ways of + browsing, searching and rendering Coq mathematical developments into a + coherent and Web-oriented architecture open to the Coq user community + and beyond.

+ +

An alternative route for the creation of content-based mathematical + information from standard digital repositories by means of a suitable + LaTeX-based authoring system will be explored by the Albert + Einstein Institute (AEI) in Golm (Germany). AEI publishes a solely + electronic review journal, Living Reviews in Relativity on + the Web, which provides refereed, regularly updated review + articles on all areas of gravitational physics. Since its + release in January 1998 the journal has become a primary + entry point for students, lecturers and researchers alike + for up-to-date information on the current status of research + in gravitational physics. Moving this unique repository and + communication forum of current physical and mathematical + knowledge in relativity to content mark-up, making it + available for semantic search, and for re-use and evaluation + e.g. in math algebra systems motivates the involvement + in the MOWGLI project. The journal will develop a + LaTeX based authoring tool interfacing with MOWGLI, and + serve as a showcase to demonstrate how content-mark-up in + mathematics improves the usability and information depth + of electronic science journals.

+ +

The AEI will be supported by the newly founded Center for Information + Management (CIM) of the Max Planck Society. The CIM has been set up + by the Society to support researchers and research processes in the area + of information management. The objectives of the project include + coordination of existing activities within the Society and + implementation of a strategy to develop electronic research archives. + The current Managing Editor of the AEI's electronic journal Living + Reviews in Relativity has been appointed executive director of the CIM + (starting from 1 Sep 2001) and will be in charge of the project management + for Tasks 4.4 and 6.3 of the proposal. The CIM will be in an + excellent position to promote dissemination and use of the project results + within the Max Planck Society. It will further give technical support to + the Dissemination Manager in providing the MOWGLI website.

+ +

Professor Wegner, Scientific Coordinator of EMIS (European + Mathematical Information Service), will also provide a main liaison with + previous and successful European Projects on digital libraries and + metadata, such as EULER + and the TRIAL Solution project (\verb+http://www.trial-solution.de+). + In particular, all the achievements of these Projects + will be integrated inside MOWGLI, as far as the respective teams + will agree to this. + Moreover, in his quality of Scientific Coordinator of EMIS, member + of the advisory board for MATHDI, and Chairman of the Electronic + Publishing Committee of European + Mathematical Society, Professor Wegner is an excellent candidate + to organise the information + dissemination and exploitation activities for the project.

+ +

In particular, the Department of Computer Science of the University of + Nijmegen will apply MOWGLI's technologies to the development of + an ``electronic book'', covering a typical undergraduate course + in Algebra or Analysis. The Department of Computer Science in Nijmegen + has a lot of experience in formal mathematics and theorem proving. + Notably, the group has done large theory developments in the theorem + prover Coq. (The FTA + project: Eindhoven University of Technology, a sub-site of Nijmegen, + has expertise in OpenMath and in using WWW technology for educational + purposes. This has resulted -- among other things -- in + IDA, the + interactive course notes in algebra where a combination of HTML + and applets is used to present the mathematics. Jointly, Nijmegen and + Eindhoven have experience in combining theorem provers and computer + algebra packages, notably Coq and GAP.

+ +

Trusted Logic (France), which is specialized in secure and + validated solutions for open systems, aims to present the + formalization and the demonstration of some security + properties related to the code embedded into a smart card. The presentation + must be in a format understandable by the company in charge of the + evaluation of the code and in accordance with the Common Criteria + standard.

+

A third pilot application is the semantic markup of the Journal + Living Reviews in Relativity published by AEI-Golm, + already mentioned above.

+ + diff --git a/helm/mowgli/home/xml/people/aei/kelley.xml b/helm/mowgli/home/xml/people/aei/kelley.xml new file mode 100644 index 000000000..d371e8825 --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/kelley.xml @@ -0,0 +1,10 @@ + + + + + + Ian + Kelley + Programmer + ??? + diff --git a/helm/mowgli/home/xml/people/aei/schutz.xml b/helm/mowgli/home/xml/people/aei/schutz.xml new file mode 100644 index 000000000..94b033716 --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/schutz.xml @@ -0,0 +1,30 @@ + + + + + + Bernard F. + Schutz + Prof. + Institute Director + Editor-in-Chief + schutz@aei-potsdam.mpg.de + http://www.aei-potsdam.mpg.de/cgi-bin/interface/people.cgi?key=schutz + +

Prof. Bernard Schutz (born in 1946 in the USA) is director of the Max + Planck Institute for Gravitational Physics (Albert Einstein Institute), + heading the Astrophysical Relativity Division of the Institute, and + Professor at Cardiff University. In acknowledgement of pioneering + scientific work in gravitational physics he has been elected Fellow of + the American Physical Society. He invented the ``Living Reviews'' concept + in 1996 and acts as the journal's Editor-in-chief. Bernard Schutz has + served on the Editorial Board of Classical and Quantum Gravity between + 1988 and 1990, and since 1998 is member of the Editorial Board of the + monograph series Studies In High Energy Physics, Cosmology and Gravitation + (Institute of Physics Publishing, Bristol, UK).

+ + + + + + diff --git a/helm/mowgli/home/xml/people/aei/velden.xml b/helm/mowgli/home/xml/people/aei/velden.xml new file mode 100644 index 000000000..094c7d4bc --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/velden.xml @@ -0,0 +1,21 @@ + + + + + + Theresa + Velden + Executive Director, CIM + velden@aei-potsdam.mpg.de + http://www.aei-potsdam.mpg.de/office/velden.html + +

Theresa Velden (born in 1970 in Germany) graduated in Physics + from Bielefeld University in 1997 after having completed a diploma + thesis on Mathematical Relativity at the Max Planck Institute + for Gravitational Physics. Since 1998 she has been leading the + editorial team of Living Reviews in Relativity as Managing + Editor, organizing the editorial process and supervising the + development of software for electronic publishing and journal + management.

+ + diff --git a/helm/mowgli/home/xml/people/aei/wegner.xml b/helm/mowgli/home/xml/people/aei/wegner.xml new file mode 100644 index 000000000..450380aa5 --- /dev/null +++ b/helm/mowgli/home/xml/people/aei/wegner.xml @@ -0,0 +1,51 @@ + + + + + + Bernd + Wegner + Prof. + Full Professor of Mathematics + Editor-in-chief of Zentralblatt MATH, the most comprehensive + literature information service in mathematics, with Web access under + EMIS + Member of the advisory board for MATHDI, an information data base on + education in mathematics + Scientific Coordinator of EMIS, the European Mathematical + Information Service, providing a mathematics portal with an electronic + library as the main conten + Leader of the TU-group for the EULER-project, which has developed a + prototype for an integrated access to Web-based mathematical documents, + funded by Telematics for Libraries, and supported by a small TAKEUP-project + for the transition to a regular Web service + Scientific Director of the LIMES-project (Large Infrastructures in + Mathematics - Enhanced Services) which is designed to transform Zentralblatt + MATH into European cooperation with Web-based input structures, funded by the + Fifth Framework Programme + Director of the ERAM-project (Electronic Research Archive in + Mathematics),funded by Deutsche Forschungsgemeinschaft and designed to build + up a digital archive of classical mathematics, capturing the Jahrbuch ueber + die Fortschritte in database as a pre-Zentalblatt access facility to the + archive + Chairman of the Electronic Publishing Committee of EMS (European + Mathematical Society) + member of the Database Committee of the EMS + associated with project Euclid (Cornell University, Ithaka, U.S.A.), + establishing a non-profit (electronic) publication facility for + mathematics + member of the board of IWI (Institute for Scientific Information in + Osnabrueck) + ??? + ??? + +

He has participated with one or more talks at about 20 events on electronic + information and communication in 2000, including continental congresses in + Lisbon, Barcelona, Rio de Janeiro, Havanna, Moscow, and Manila. He has been + elected as member of the scientific committee for several conferences on + the subject in 2001: (Crimea, Athens, Coimbra, Linz, Guatemala City) and + received invitations for plenary lectures at additional conferences.

+

These activities give an excellent background to organise the information + dissemination and exploitation activities for the project.

+ + diff --git a/helm/mowgli/home/xml/people/bologna/asperti.xml b/helm/mowgli/home/xml/people/bologna/asperti.xml new file mode 100644 index 000000000..da04f8154 --- /dev/null +++ b/helm/mowgli/home/xml/people/bologna/asperti.xml @@ -0,0 +1,55 @@ + + + + + + Andrea + Asperti + Prof. + Full Professor of Formal Languages and Compilers + Member of the Advisory Committee of the World Wide Web + Former Director of the Undergraduate Program in Computer Science + of the University of Bologna + Responsible of the Bologna site for the European TMR Project + LINEAR + Former Responsible of the Bologna site for the WG-21836 + CONFER-II + Main Responsible for the Nation Research Project Linear Logic and + beyond + asperti@cs.unibo.it + http://www.cs.unibo.it/~asperti +
Dipartimento di Scienze dell'Informazione, Via di Mura Anteo Zamboni 7, Bologna, Italy
+ +39 51 35 45 05 + +

Andrea Asperti was born in Italy, in 1961. He was awarded a Ph.D in + Computer Science by the University of Pisa in 1989. In the same year + he obtained a post-doc position at INRIA-Rocquencourt, where he was + employed as a researcher in 1991. In 1992 he obtained the chair + of Formal Languages and Compilers at the Department of + Computer Science of the University of Bologna, becoming + Full Professor in year 2000. + He is currently teaching courses on Programming Languages, + Theoretical Computer Science and Human-Computer Interaction.

+ + +

The research interests of Andrea Asperti are focused on forms, + formats and methods of knowledge representation and elaboration. + This covers Markup Languages, Information Processing, + Programming Languages, Interpreters and + Compilers, Type Systems, Higher-order Logics, Linear Logic, Category + Theory. He is author of over 40 international publications on formal + aspects of the theory of Computing, and several books.

+

He has been member of the Programme Committees of several + International Conferences, comprising CONCUR'98, RTA'99, + LICS'99, PPDP'00, CSL'01, MKM'01 (First International Workshop + on Mathematical Knowledge Management).

+

His recent scientific activity has been mostly focused on the + HELM Project, aimed to build the technological infrastructure + for an Hypertextual Electronic Library of Mathematics.

+ + + + + + + diff --git a/helm/mowgli/home/xml/people/bologna/guidi.xml b/helm/mowgli/home/xml/people/bologna/guidi.xml new file mode 100644 index 000000000..ace5d05d5 --- /dev/null +++ b/helm/mowgli/home/xml/people/bologna/guidi.xml @@ -0,0 +1,17 @@ + + + + + + Ferruccio + Guidi + Ph.D. Student + fguidi@cs.unibo.it + http://www.cs.unibo.it/~fguidi +
Dipartimento di Scienze dell'Informazione, Via di Mura Anteo Zamboni 7, Bologna, Italy
+ +39 51 20 94 871 + + + + + diff --git a/helm/mowgli/home/xml/people/bologna/padovani.xml b/helm/mowgli/home/xml/people/bologna/padovani.xml new file mode 100644 index 000000000..68f4a5bb9 --- /dev/null +++ b/helm/mowgli/home/xml/people/bologna/padovani.xml @@ -0,0 +1,18 @@ + + + + + + Luca + Padovani + Ph.D. Student + Member of MathML-WG + lpadovan@cs.unibo.it + http://www.cs.unibo.it/~lpadovan +
Dipartimento di Scienze dell'Informazione, Via di Mura Anteo Zamboni 7, Bologna, Italy
+ +39 51 20 94 871 + + + + + diff --git a/helm/mowgli/home/xml/people/bologna/sacerdoti.xml b/helm/mowgli/home/xml/people/bologna/sacerdoti.xml new file mode 100644 index 000000000..f613cfa1b --- /dev/null +++ b/helm/mowgli/home/xml/people/bologna/sacerdoti.xml @@ -0,0 +1,17 @@ + + + + + + Claudio + Sacerdoti Coen + Ph.D. Student + sacerdot@cs.unibo.it + http://www.cs.unibo.it/~sacerdot +
Dipartimento di Scienze dell'Informazione, Via di Mura Anteo Zamboni 7, Bologna, Italy
+ +39 51 20 94 871 + + + + + diff --git a/helm/mowgli/home/xml/people/bologna/schena.xml b/helm/mowgli/home/xml/people/bologna/schena.xml new file mode 100644 index 000000000..304f188e8 --- /dev/null +++ b/helm/mowgli/home/xml/people/bologna/schena.xml @@ -0,0 +1,18 @@ + + + + + + Irene + Schena + Ph.D. Student + Member of MathML-WG + schena@cs.unibo.it + http://www.cs.unibo.it/~schena +
Dipartimento di Scienze dell'Informazione, Via di Mura Anteo Zamboni 7, Bologna, Italy
+ +39 51 20 94 871 + + + + + diff --git a/helm/mowgli/home/xml/people/dfki/kohlhase.xml b/helm/mowgli/home/xml/people/dfki/kohlhase.xml new file mode 100644 index 000000000..7544fc839 --- /dev/null +++ b/helm/mowgli/home/xml/people/dfki/kohlhase.xml @@ -0,0 +1,11 @@ + + + + + + Michael + Kohlhase + Dr. + kohlhase@cs.cmu.edu + http://www.ags.uni-sb.de/~kohlhase/ + diff --git a/helm/mowgli/home/xml/people/dfki/melis.xml b/helm/mowgli/home/xml/people/dfki/melis.xml new file mode 100644 index 000000000..849a256d9 --- /dev/null +++ b/helm/mowgli/home/xml/people/dfki/melis.xml @@ -0,0 +1,29 @@ + + + + + + Erica + Melis + PD. Dr. + Senior Researcher at the German Research Center for Artificial + Intelligence (DFKI GmbH) + melis@dfki.de + http://www.ags.uni-sb.de/~melis + +

Erica Melis is a Senior Researcher at the German + Research Center for Artificial Intelligence (DFKI GmbH). She was a + research scientist at the School of Computer Science of Carnegie Mellon + University and at the Department of AI at the University of Edinburgh. + Later she has been an Assistant Professor at the University of Saarland + and is member of a Sonderforschungsbereich in Saarbruecken. She served on + numerous programme committees. Erica Melis is the editor of proceedings + and the co/author of numerous scientific papers in journals, conferences, + and collections in areas such as deduction, planning, case-based + reasoning, intelligent tutor systems.

+

Currently, her research interests focus proof planning and on the + application of Artificial Intelligence technology in intelligent learning + environments.

+

She is a member of AAAI and GI.

+ + diff --git a/helm/mowgli/home/xml/people/dfki/siekmann.xml b/helm/mowgli/home/xml/people/dfki/siekmann.xml new file mode 100644 index 000000000..de5918435 --- /dev/null +++ b/helm/mowgli/home/xml/people/dfki/siekmann.xml @@ -0,0 +1,33 @@ + + + + + + Joerg + Siekmann + Prof. + Professor of Computer Science + Director of the Deduction and Multiagent Systems research + department at the DFKI + Joerg.Siekmann@dfki.de + http://www.dfki.de/~siekmann + +

Prof. Dr. Joerg Siekmann is Professor of Computer + Science and Director of the Deduction and Multiagent Systems research + department at the DFKI. He studied at the University of Goettingen + (Mathematics and Physics, 1972) and the University of Essex (M.Sc. in + Computer Science, 1973, and Ph.D. in Computer Science, 1976). From 1976 + to 1983 he was a research assistant at the University of Karlsruhe. + From 1983 to 1991 he was Professor of Computer Science at the University + of Kaiserslautern and since 1991 he has a joint position as professor for + Computer Science at the Universitaet des Saarlandes and as one of the + directors at the DFKI. He has published widely in AI, Automated Reasoning + and Unification Theory and served on many programme committees and was + programme chairman of various conferences (such as CADE, KI etc.). He is + editor of several logic and AI oriented scientific journals (such + as Journal of Automated Reasoning, Journal of Artificial Intelligence, + Journal of Logic and Computation etc). His biography is included + in most international Whos Who, as one of the founders of AI in + Germany.

+ + diff --git a/helm/mowgli/home/xml/people/inria/amerkad.xml b/helm/mowgli/home/xml/people/inria/amerkad.xml new file mode 100644 index 000000000..b6cd54de3 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/amerkad.xml @@ -0,0 +1,11 @@ + + + + + + Hugo + Herbelin + Prof. + Hugo.Herbelin@inria.fr + http://pauillac.inria.fr/~herbelin + diff --git a/helm/mowgli/home/xml/people/inria/bertot.xml b/helm/mowgli/home/xml/people/inria/bertot.xml new file mode 100644 index 000000000..6ad788c9b --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/bertot.xml @@ -0,0 +1,11 @@ + + + + + + Yves + Bertot + Researcher + Yves.Bertot@sophia.inria.fr + http://www-sop.inria.fr/lemme/Yves.Bertot + diff --git a/helm/mowgli/home/xml/people/inria/chicli.xml b/helm/mowgli/home/xml/people/inria/chicli.xml new file mode 100644 index 000000000..095ad4141 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/chicli.xml @@ -0,0 +1,11 @@ + + + + + + Laurent + Chicli + Ph.D. Student + Laurent.Chicli@sophia.inria.fr + http://www-sop.inria.fr/lemme/Laurent.Chicli + diff --git a/helm/mowgli/home/xml/people/inria/delahaye.xml b/helm/mowgli/home/xml/people/inria/delahaye.xml new file mode 100644 index 000000000..b25f922ca --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/delahaye.xml @@ -0,0 +1,11 @@ + + + + + + David + Delahaye + Ph.D. Student + David.Delahaye@inria.fr + http://pauillac.inria.fr/~delahaye + diff --git a/helm/mowgli/home/xml/people/inria/herbelin.xml b/helm/mowgli/home/xml/people/inria/herbelin.xml new file mode 100644 index 000000000..d8bb383a2 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/herbelin.xml @@ -0,0 +1,18 @@ + + + + + + Hugo + Herbelin + Prof. + Associate Professor at University Paris 10 + Seconded at INRIA + Hugo.Herbelin@inria.fr + http://pauillac.inria.fr/~herbelin +
Domaine de Voluceau, 78153 Rocquencourt Cedex, France
+ +33 (0) 1 39 63 53 77 + +

Born June 9, 1967.

+ + diff --git a/helm/mowgli/home/xml/people/inria/naciri.xml b/helm/mowgli/home/xml/people/inria/naciri.xml new file mode 100644 index 000000000..95dd74103 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/naciri.xml @@ -0,0 +1,11 @@ + + + + + + Hanane + Naciri + Ph.D. Student + Hanane.Naciri@sophia.inria.fr + http://www-sop.inria.fr/lemme/Hanane.Naciri + diff --git a/helm/mowgli/home/xml/people/inria/pottier.xml b/helm/mowgli/home/xml/people/inria/pottier.xml new file mode 100644 index 000000000..312719f85 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/pottier.xml @@ -0,0 +1,11 @@ + + + + + + Loic + Pottier + Researcher + Loic.Pottier@sophia.inria.fr + http://www-sop.inria.fr/lemme/Loic.Pottier + diff --git a/helm/mowgli/home/xml/people/inria/rideau.xml b/helm/mowgli/home/xml/people/inria/rideau.xml new file mode 100644 index 000000000..06c52ce86 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/rideau.xml @@ -0,0 +1,11 @@ + + + + + + Laurence + Rideau + Researcher + Laurece.Rideau@sophia.inria.fr + http://www-sop.inria.fr/lemme/Laurece.Rideau + diff --git a/helm/mowgli/home/xml/people/inria/thery.xml b/helm/mowgli/home/xml/people/inria/thery.xml new file mode 100644 index 000000000..79caf6f77 --- /dev/null +++ b/helm/mowgli/home/xml/people/inria/thery.xml @@ -0,0 +1,11 @@ + + + + + + Laurent + Thery + Researcher + Laurent.Thery@sophia.inria.fr + http://www-sop.inria.fr/lemme/Laurente.Thery + diff --git a/helm/mowgli/home/xml/people/nijmegen/barendregt.xml b/helm/mowgli/home/xml/people/nijmegen/barendregt.xml new file mode 100644 index 000000000..339462738 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/barendregt.xml @@ -0,0 +1,12 @@ + + + + + + Henk + Barendregt + Prof. + Full Professor, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/barreiro.xml b/helm/mowgli/home/xml/people/nijmegen/barreiro.xml new file mode 100644 index 000000000..bea79cb95 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/barreiro.xml @@ -0,0 +1,11 @@ + + + + + + Ernesto Reinaldo + Barreiro + Ph.D. Student, Eindhoven + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/cohen.xml b/helm/mowgli/home/xml/people/nijmegen/cohen.xml new file mode 100644 index 000000000..447c6b428 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/cohen.xml @@ -0,0 +1,12 @@ + + + + + + Arjeh + Cohen + Prof. + Full Professor, Eindhoven + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/cruz-filipe.xml b/helm/mowgli/home/xml/people/nijmegen/cruz-filipe.xml new file mode 100644 index 000000000..febda7158 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/cruz-filipe.xml @@ -0,0 +1,11 @@ + + + + + + Luiz + Crus-Filipe + Ph.D. Student, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/geuvers.xml b/helm/mowgli/home/xml/people/nijmegen/geuvers.xml new file mode 100644 index 000000000..d0abc1876 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/geuvers.xml @@ -0,0 +1,47 @@ + + + + + + Herman + Geuvers + Prof. + Associate Professor in Foundations of Mathematics and Computer + Science + Responsible for the Nijmegen-Utrecht site of the EC Thematic + Network ``TYPES'' (Computer Assisted Reasoning Based on Type Theory), + IST-1999-29001 + President of the education committee of the Sub-faculty of + Computer Science at the University of Nijmegen + Former member of the Management Board of the Dutch + research school IPA (Institute for Programming Research and + Algorithmics) + herman@cs.kun.nl + http://www.cs.kun.nl/~herman +
Faculteit NWI, KUN, Toernooiveld 1, 6525 ED Nijmegen, NL
+ +31 243 652603 + +

Herman Geuvers studied Mathematics at the University of Nijmegen and + got his Ph.D. in Mathematics and Computer Science in 1993 at the same + University. In the same year he became assistant professor in computer + science at the Eindhoven University of Technology in the Formal + Methods group. From January 1st 2000, he is associate professor at the + Department of Computer Science of the University of Nijmegen in the + Foundations group. He is currently teaching in Formal Languages and + Computability and Type Theory.

+ + +

The research interests of Herman + Geuvers are: Formalization of Mathematics, Interactive Theorem + Proving, Higher-order Logics, Communicating Formal Mathematics, Type + Theory and lambda-calculus. His recent scientific activities range from + the study of formal theories (especially typed lambda-calculi) to + doing large theory developments in theorem provers, notably the + formalization of the fundamental theorem of algebra in Coq.

+ + + + + + + diff --git a/helm/mowgli/home/xml/people/nijmegen/niqui.xml b/helm/mowgli/home/xml/people/nijmegen/niqui.xml new file mode 100644 index 000000000..723dbf3bd --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/niqui.xml @@ -0,0 +1,11 @@ + + + + + + Milan + Niqui + Ph.D. student, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/stein.xml b/helm/mowgli/home/xml/people/nijmegen/stein.xml new file mode 100644 index 000000000..cff0c62e5 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/stein.xml @@ -0,0 +1,11 @@ + + + + + + Jasper + Stein + Ph.D. Student, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/synek.xml b/helm/mowgli/home/xml/people/nijmegen/synek.xml new file mode 100644 index 000000000..4861a6991 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/synek.xml @@ -0,0 +1,11 @@ + + + + + + Dan + Synek + Programmer, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/nijmegen/wiedijk.xml b/helm/mowgli/home/xml/people/nijmegen/wiedijk.xml new file mode 100644 index 000000000..7aec7ad04 --- /dev/null +++ b/helm/mowgli/home/xml/people/nijmegen/wiedijk.xml @@ -0,0 +1,12 @@ + + + + + + Freek + Widijk + Dr. + Post Doc Researcher, Nijmegen + ??? + ??? + diff --git a/helm/mowgli/home/xml/people/person.dtd b/helm/mowgli/home/xml/people/person.dtd new file mode 100644 index 000000000..94e4c6d05 --- /dev/null +++ b/helm/mowgli/home/xml/people/person.dtd @@ -0,0 +1,28 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/mowgli/home/xml/people/trusted-logic/bolignano.xml b/helm/mowgli/home/xml/people/trusted-logic/bolignano.xml new file mode 100644 index 000000000..1df338629 --- /dev/null +++ b/helm/mowgli/home/xml/people/trusted-logic/bolignano.xml @@ -0,0 +1,43 @@ + + + + + + Dominique + Bolignano + Chairman and Chief Executive Officer of Trusted Logic + Part-time Full Professor at the Université Paris-Dauphine + Dominique.Bolignano@trusted-logic.fr + +

Dominique Bolignano is Chairman and Chief Executive Officer of + Trusted Logic. He also teaches security and languages as a part-time + full professor (Professeur Associé) at the Université Paris-Dauphine. + From 1996 to 1999, Dominique Bolignano worked with Dyade, a joint + venture between Bull and INRIA (French National Research Institute + in Computer Science and Control), as Director, Responsible for + technology transfer in security, electronic commerce, and smart cards, + and Project Director in the following areas : formal verification of + electronic commerce protocols (and more generally cryptographic protocols), + evaluation or design of security architectures (mainly for secure + embedded systems, such as smart cards, payment terminals, GSM phones, + etc.), development of highly secure Java Virtual Machines (Bull Odyssey + JavaCard, payment terminals), formal methods for ITSEC and Common + Criteria security evaluations (participation to various security + evaluations including some on smart cards operating systems). + Before that, Dominique Bolignano was the head of a research group + in the Corporate Research Centre of Bull and he has acquired, from + 1982 to 1996, a deep experience in industry software development and + formal verification systems (distributed systems, security protocols). + Dominique Bolignano takes part in the Java Card Forum. He also is a + Member of the newly created IFIP Working group on Foundations of Security + Analysis and Design. He has been an invited speaker at MFPS'98, CAV'99, + CARI'98, CIRM'98, JFMM'98, RTCS'96, Cartier'96, FemSys'97, and to many + security or formal methods symposia and presented invited tutorials at + Forte'98, Cartier'96, Forte'93. Dominique Bolignano also acted as a PhD + advisor, as a reviewer and evaluator for European Community programs. + He is a reviewer in several journals (Journal of Theoretical + Computer Science (TCS), TSI, ...) and has been a reviewer and/or + a member of the Program Committee in international + conferences (SESS'93, FME'96,VDM 91 et FORTE 92, SaS'94, ...)

+ + diff --git a/helm/mowgli/home/xml/project.xml b/helm/mowgli/home/xml/project.xml new file mode 100644 index 000000000..348a636f0 --- /dev/null +++ b/helm/mowgli/home/xml/project.xml @@ -0,0 +1,20 @@ + + + + + + + + + +]> + + + Mathematics On the Web: Get it by Logic and Interfaces + MOWGLI + Information Society Technologies Programme + IST + IST-2001-33562 MOWGLI + ??? + diff --git a/helm/mowgli/home/xml/publications/others/category_al.xml b/helm/mowgli/home/xml/publications/others/category_al.xml new file mode 100644 index 000000000..ffeab60cd --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/category_al.xml @@ -0,0 +1,15 @@ + + + + + + Categories, Types and Structures. An introduction to Category + Theory for the Working Computer Scientist. + + + Giuseppe + Longo + + Foundation of Computing Series, Massachusetts Institute of Technology + Press, ISBN 0 262 01125-5, 1991 + diff --git a/helm/mowgli/home/xml/publications/others/crimea2001_apss.xml b/helm/mowgli/home/xml/publications/others/crimea2001_apss.xml new file mode 100644 index 000000000..1f151a612 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/crimea2001_apss.xml @@ -0,0 +1,15 @@ + + + + + + Formal Mathematics on the Web + + + + + Proceedings of the Eighth International Conference on + "Libraries and Associations in the Transient World: + New Technologies and New Forms of Cooperation", June 9-17, 2001, + Sudak, Autonomous Republic of Crimea, Ukraine + diff --git a/helm/mowgli/home/xml/publications/others/cup_s.xml b/helm/mowgli/home/xml/publications/others/cup_s.xml new file mode 100644 index 000000000..2299f18d2 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/cup_s.xml @@ -0,0 +1,9 @@ + + + + + + A First Course in General Relativity + + Cambridge University Press, Cambridge (1985) + diff --git a/helm/mowgli/home/xml/publications/others/cup_s2.xml b/helm/mowgli/home/xml/publications/others/cup_s2.xml new file mode 100644 index 000000000..353ee5913 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/cup_s2.xml @@ -0,0 +1,9 @@ + + + + + + Geometrical methods of mathematical physics + + Cambridge University Press, Cambridge, (1980) + diff --git a/helm/mowgli/home/xml/publications/others/extreme2001_apss.xml b/helm/mowgli/home/xml/publications/others/extreme2001_apss.xml new file mode 100644 index 000000000..43e30b009 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/extreme2001_apss.xml @@ -0,0 +1,13 @@ + + + + + + XML, Stylesheets and the re-mathematization of Formal Content + + + + + Proceedings of ``Extreme Markup Languages 2001 Conference'', + August 12-17, 2001, Montr'eal, Canada. + diff --git a/helm/mowgli/home/xml/publications/others/har_bg.xml b/helm/mowgli/home/xml/publications/others/har_bg.xml new file mode 100644 index 000000000..2896fc308 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/har_bg.xml @@ -0,0 +1,11 @@ + + + + + + Proof Assistants using Dependent Type Systems + + + to appear as a chapter of the Handbook of Automated Reasoning, eds. + A. Robinson and A. Voronkov, Elsevier 2001 + diff --git a/helm/mowgli/home/xml/publications/others/jep_ws.xml b/helm/mowgli/home/xml/publications/others/jep_ws.xml new file mode 100644 index 000000000..43064e5b9 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/jep_ws.xml @@ -0,0 +1,13 @@ + + + + + + Making an Electronic Journal Live + + J. + Wheary + + + Journal of Electronic Publishing, vol.3, is. 1, September (1997). (http://www.press.umich.edu/jep/03-01/LR.html) + diff --git a/helm/mowgli/home/xml/publications/others/jep_wwsw.xml b/helm/mowgli/home/xml/publications/others/jep_wwsw.xml new file mode 100644 index 000000000..dfb77dcb7 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/jep_wwsw.xml @@ -0,0 +1,22 @@ + + + + + + Thinking and Developing Electronically + + J. + Wheary + + + L. + Wild + + + + C. + Weyher + + Journal of Electronic Publishing, vol.4, is. 2, December (1998). + (http://www.press.umich.edu/jep/04-02/wheary2.html) + diff --git a/helm/mowgli/home/xml/publications/others/jlp2001_scg.xml b/helm/mowgli/home/xml/publications/others/jlp2001_scg.xml new file mode 100644 index 000000000..abb8b1578 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/jlp2001_scg.xml @@ -0,0 +1,18 @@ + + + + + + The logic and mathematics of occasion sentences + + P.A.M. + Seuren + + + Venanzio + Capretta + + + The logic and mathematics of occasion sentences, to appear in the + Journal of Linguistics and Philosophy, 2001 + diff --git a/helm/mowgli/home/xml/publications/others/mathml2000_apss.xml b/helm/mowgli/home/xml/publications/others/mathml2000_apss.xml new file mode 100644 index 000000000..67d49461a --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/mathml2000_apss.xml @@ -0,0 +1,13 @@ + + + + + + Formal Mathematics in MathML + + + + + First MathML International Conference, October 20-21, 2000, + Urbana-Champaign, IL, USA. + diff --git a/helm/mowgli/home/xml/publications/others/mscs_gb.xml b/helm/mowgli/home/xml/publications/others/mscs_gb.xml new file mode 100644 index 000000000..504d68d97 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/mscs_gb.xml @@ -0,0 +1,15 @@ + + + + + + Some logical and syntactical observations concerning the first + order dependent type system lambda P + + + E. + Barendsen + + Mathematical Structures in Computer Science, vol. 9-4, 1999, + pp. 335 -- 360 + diff --git a/helm/mowgli/home/xml/publications/others/publication.dtd b/helm/mowgli/home/xml/publications/others/publication.dtd new file mode 100644 index 000000000..5fff8ba8d --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/publication.dtd @@ -0,0 +1,13 @@ + + + + + + + + + + + + diff --git a/helm/mowgli/home/xml/publications/others/tcs2001_og.xml b/helm/mowgli/home/xml/publications/others/tcs2001_og.xml new file mode 100644 index 000000000..2844b10d8 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/tcs2001_og.xml @@ -0,0 +1,13 @@ + + + + + + Proof by Computation in the Coq system + + M. + Oostdijk + + + To appear in Theoretical Computer Science, 2001 + diff --git a/helm/mowgli/home/xml/publications/others/tphols2000_gwz.xml b/helm/mowgli/home/xml/publications/others/tphols2000_gwz.xml new file mode 100644 index 000000000..470731062 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/tphols2000_gwz.xml @@ -0,0 +1,15 @@ + + + + + + Equational Reasoning via Partial Reflection + + + + J. + Zwanenburg + + Theorem Proving for Higher Order Logics, TPHOL 2000, Portland OR, USA, + eds. M. Aagaard and J. Harrison, LNCS 1869, pp. 162 -- 178 + diff --git a/helm/mowgli/home/xml/publications/others/tphols2001_apss.xml b/helm/mowgli/home/xml/publications/others/tphols2001_apss.xml new file mode 100644 index 000000000..14154d3a8 --- /dev/null +++ b/helm/mowgli/home/xml/publications/others/tphols2001_apss.xml @@ -0,0 +1,14 @@ + + + + + + HELM and the semantic Math-Web + + + + + Proceedings of the 14th International Conference on Theorem + Proving in Higher Order Logics (TPHOLS 2001), 3-6 September 2001, + Edinburgh, Scotland + diff --git a/helm/mowgli/home/xml/sites/aei.xml b/helm/mowgli/home/xml/sites/aei.xml new file mode 100644 index 000000000..8973a830c --- /dev/null +++ b/helm/mowgli/home/xml/sites/aei.xml @@ -0,0 +1,74 @@ + + + + + + + Max Planck Institute for Gravitational Physics (Albert Einstein + Institute) + Germany + http://www.aei.mpg.de +
Am Muhlenberg 1, 14476 Golm, Germany
+ + +

Since 1998 the Max Planck Institute for Gravitational Physics, which is + devoted to basic research in relativity, publishes one of the most + innovative electronic science journals, {\em Living Reviews in + Relativity} (http://www.livingreviews.org). Its mission is to build the + journal into a primary reference point in the field, exploiting new and + cutting edge Web technologies to maximise use, transparency, and depth + of the information provided. The Institute has a number of staff who + are exceptionally skilled in computing, and many of them contributed to + the development of software that has made the journal's Web site one of + the most advanced in the world of electronic publishing. Further + background information on the journal can be found at + http://www.livingreviews.org/Project/index.html. Fast and effective + international dissemination of the Web journal is provided by the + European Mathematical Society's Information Service, which maintains a + network of more than 30 mirror servers worldwide

+

The Institute has close connections to the newly founded Center for + Information Management of the Max Planck Society that will act as a + central service to the more than 80 Max Planck Institutes, to improve + their ability to access and to publish information on the Internet. It + is further cooperating with the leading European publisher of original + research in gravitational physics, the Institute of Physics Publishing + (Bristol, UK) with its journal {\em Classical and Quantum Relativity}.

+

The Max Planck Institute for Gravitational Physics will join forces + with Professor Bernd Wegner at the Technical University in Berlin. + Both parties are currently cooperating in the dissemination and + mirroring of electronic journals like + {\em Living Reviews in Relativity}.

+ + + + + + Center for Information Management in the Max Planck Society + Germany + http://www.zim.mpg.de +
c/o Max Planck Society, Hofgartenstrasse 8, PF 10 10 62, + D-80084 Munich, Germany
+ + +

The mission of the new Center for Information Management of the Max + Planck Society is to allow the Society with its more than 80 + specialized research Institutes to keep pace with and eventually play + a leadership role in Europe in the management of scientific information. + It will be staffed with 6 employees and start operating in September + 2001. The project will be advised by a commission of MPG Institute + directors and Rick Luce, the Director of the Los Alamos National + Laboratory's "Library Without Walls".

+ + + + TU Berlin + Germany + http://www.emis.de +
Fachbereich Mathematik, Technische Universität Berlin, + Straße des 17. Juni 135, D - 10623 Berlin
+ + +

???

+ + + diff --git a/helm/mowgli/home/xml/sites/bologna.xml b/helm/mowgli/home/xml/sites/bologna.xml new file mode 100644 index 000000000..b145c49ff --- /dev/null +++ b/helm/mowgli/home/xml/sites/bologna.xml @@ -0,0 +1,51 @@ + + + + + + University of Bologna (Italy), Department of Computer Science + Italy + http://www.cs.unibo.it +
Via di mura Anteo Zamboni VII, 40127, Bologna, ITALY
+ + +

The Department of Computer Science of Bologna is the + only educational institution in Italy to be affiliated + to the World Wide Web Consortium (and one of the few + members of this category in Europe). This affiliation + testifies the interest, both technical and didactic, + traditionally devoted by our Department to Web technologies, + Internet and, more generally, distributed computing. + This is joined to a solid expertise in programming + languages, algorithms, theory and formal methods, + that provides a very stimulating and dialectical environment + for research. + The Department is in charge of an undergraduate + Program in Computer Science, with more than three hundreds new + students a year, and a graduate Ph.D. Program, currently + comprising sixteen students.

+ + + Hypertextual Library of Mathematics + HELM + http://www.cs.unibo.it/helm + + + + + + +

The Hypertextual Electronic Library of Mathematics Project + is active in Bologna since 1999. Its aim is the development of a suitable + technology for the creation and maintenance of a virtual, distributed, + hypertextual library of formal mathematical knowledge. As a subsidiary + goal, HELM is meant to integrate the current tools for the automation of + formal reasoning and the mechanisation of mathematics (proof assistants + and logical frameworks) with the most recent technologies for the + development of Web applications and electronic publishing, taking + advantage of the potentiality offered by XML Technologies. + The Project is developed in tight cooperation with the W3C + MathML Working Group, which we are a member of.

+ + + diff --git a/helm/mowgli/home/xml/sites/dfki.xml b/helm/mowgli/home/xml/sites/dfki.xml new file mode 100644 index 000000000..ae082ab7b --- /dev/null +++ b/helm/mowgli/home/xml/sites/dfki.xml @@ -0,0 +1,62 @@ + + + + + + German Research Center for Artificial Intelligence, GmbH, DFKI + Germany + http://www.dfki.uni-sb.de +
???
+ + +

The German Research Center for Artificial Intelligence + GmbH, DFKI was founded in 1988. Today, DFKI is one of the largest + non-profit contract research institutes in the field of innovative + software technology based on Artificial Intelligence (AI) methods. DFKI + is focusing on the complete cycle of innovation - from world-class basic + research and technology development through leading-edge demonstrators + and prototypes to product functions and commercialization. Based in + Kaiserslautern and Saarbr{\"u}cken, the German Research Center for + Artificial Intelligence ranks among the important ``Centers of + Excellence'' worldwide. The key directors of DFKI are Prof. Dr. Wolfgang + Wahlster (CEO) and Dr. Walter G. Olthoff (CFO).DFKI's mission is + technology transfer, that is to move innovations in AI as quickly as + possible from the lab into the marketplace by maintaining research + projects at the forefront of science. Expertise and experience of the + company DFKI has strong expertise in each of the following domains:

+
    +
  • Information Management and Document Analysis (Director: Prof. Dr. + Andreas Dengel)
    • +
  • Intelligent Visualization and Simulation Systems + (Director: Prof. Dr. Hans Hagen)
    • +
  • Deduction and Multiagent Systems (Director: Prof. + Dr. Jorg Siekmann)
    • +
  • Language Technology (Director: Prof. Dr. Hans Uszkoreit)
    • +
  • Intelligent User Interfaces (Director: Prof. Dr. + Wolfgang Wahlster)
    • +
+

DFKI is involved in numerous industrial, academian + projects including projects in the current EC IST programme dealing with + research and development in the broad areas of intelligent interface + agents, and multiagent systems for applications in supply-chain + management, virtual enterprises, e-commerce and advanced information + systems. The partners of the DFKI are leading large-scale + concerns such as DaimlerChrysler, SAP, and Alcatel, plus the two + universities of Kaiserlautern and Saarbrucken. In the range of + medium-sized firms INSIDERS, IDS Scheer, Tecmath and KIBG are to be added. + Finally, the two most important large-scale research centers on + international level, i.e. the Fraunhofer Society and GMD, round off the + circle of partners. DFKI is part of several European Networks of + Excellence such as AgentLink and CompuLog.

+

Recently, an Education Technology Group of DFKI, headed + by Prof. J.H. Siekmann, has been established. It has carried out basic + research and applications in several fields of AI, including presentation + planning (for education material), user modeling, proof planning, + knowledge representation (for educational and mathematical Web-documents) + and integration of (mathematical services). Its main prototypical product + so far has been the Web-based, user-adaptive, generative learning + environment ActiveMath that integrates several external services. + Members of the group are actively involved in the international academic + life by organizing or contributing to conferences and workshops.

+ + diff --git a/helm/mowgli/home/xml/sites/inria.xml b/helm/mowgli/home/xml/sites/inria.xml new file mode 100644 index 000000000..28659d4f9 --- /dev/null +++ b/helm/mowgli/home/xml/sites/inria.xml @@ -0,0 +1,119 @@ + + + + + + Institut National de Recherche en Informatique et Automatique (INRIA) + Rocquencourt + France + http://www.inria.fr +
Domaine de Voluceau, 78153 Rocquencourt Cedex, France
+ + +

INRIA (National Institute for Research in Computer Science and + Control) is a French public-sector scientific and technological + institute operating under the dual authority of the Ministry of + Research and the Ministry of Industry. INRIA's missions are ``to + undertake basic and applied research, to design experimental systems, + to ensure technology and knowledge transfer, to organise international + scientific exchanges, to carry out scientific assessments, and to + contribute to standardisation''.

+

The research carried out at INRIA brings together experts from the + fields of computer science and applied mathematics covering the + following areas: Networks and Systems; Software Engineering and + Symbolic Computing; Man-Machine Interaction; Image Processing, Data + Management, Knowledge Systems; Simulation and Optimisation of Complex + Systems.

+

INRIA gathers in its premises around 2 100 persons including 1 600 + scientists , many of which belong to partner organisations (CNRS, + industrial labs, universities) and are assigned to work in common + ``projects''. On INRIA's budget, around 500 full-time equivalent R&D + positions can be accounted for.

+

A large number of INRIA senior researchers are involved in teaching + and their PhD students (about 550) prepare their thesis within the + different INRIA research projects (currently 74).

+

Its budget is roughly 90 MEuro, 20% of which comes from research and + development contracts, royalties and sales. Industrial relations are + strategic for INRIA:

+
+
Industrial contracts and European Projects.
+
Numerous industrial partners contract with the Institute for + collaborative research. They are French or foreign + companies, of all sizes. 400 such contracts are presently + active. Roughly 40% of these contracts are European funded + ones. Since 1984, 250 European Framework-Programme (FP) + projects have been executed.
+ +
Technology companies.
+
As the ultimate step in technology transfer, researchers are party to + the setting up of companies in order to implement their + technology on the market. Thirty seven spin-off companies + have been created since 1984. In 1999, INRIA has launched + two subsidiaries to promote high-tech start-up companies: + INRIA-TRANSFERT deals with early accompaniment of the + future companies, whereas I-SOURCE GESTION provides for + ``seed-money''.
+
+

INRIA is a member of ERCIM EEIG, European Research Consortium for + Computer Science and Mathematics. Outside Europe, INRIA also has a + significant activity: it has created joint research laboratories + (Russia and China), signed cooperation agreements (NSF, India, Brazil, + etc.) and promotes intensive scientific exchanges.

+ + + Lemme + ??? + + + + + + + + +

The purpose of the Lemme project is to introduce and develop formal + methods for use in writing scientific computing software. In scientific + computing, algorithms and mathematics are at the forefront. We are thus + developing tools and methods to help producing correct programs starting + from the usual mathematical descriptions of data, algorithms, properties + and proofs, structured into four research themes:

+
    +
  • Proof environments (development of the Pcoq system in Java and its + compatibility with XML/MathML).
    • +
  • Formalisation of mathematical theories (algebraic geometry, elementary + algebra and analysis).
    • +
  • Certified implementation of scientific computing algorithms (computer + algebra, arithmetics, logic).
    • +
  • Proofs on semantics of programming languages (Javacard).
    • +
+

The project belongs to the European working group Types, and to the + French action AOC (Arithm\'etique des Ordinateurs Certifiée). It keeps + up industrial collaborations with Dassault-Aviation (program proof + environments), Alcatel Space Industry (certified numerical code), and + GemPlus (Javacard certification), and also collaborates with teachers at + university on the use of formal proofs and Web-based environments in + mathematics courses.

+ + + + LogiCal + http://www.logical.inria.fr + + + +

The LogiCal team of INRIA is working on theoretical and practical + aspects of mathematical proofs. It develops the Coq proof assistant, + an implementation of an expressive formalism called Calculus of + Inductive Constructions. Coq is used both for development of formal + mathematics and for certification of programs, especially protocols + and critical systems.

+

The LogiCal project is a joint project with University Paris 11. It + is involved in the European TYPES working group and in several French + actions. Especially, it is involved in the S-Java action aiming at + certifying safety properties for JavaCard programs, in a project + aiming at certifying algorithms used in computer algebra + systems. LogiCal collaborates also on proof automation with France + Telecom.

+ + + diff --git a/helm/mowgli/home/xml/sites/nijmegen.xml b/helm/mowgli/home/xml/sites/nijmegen.xml new file mode 100644 index 000000000..732938fc3 --- /dev/null +++ b/helm/mowgli/home/xml/sites/nijmegen.xml @@ -0,0 +1,57 @@ + + + + + + Katholieke Universiteit Nijmegen + The Netherlands + http://www.cs.kun.nl +
Subfaculteit Informatica, + Faculteit Natuurwetenschappen, Wiskunde en Informatica, + Katholieke Universiteit Nijmegen, + Toernooiveld 1, 6525 ED Nijmegen, The Netherlands
+ + +

The Sub-faculty of Computer Science at the University of Nijmegen hosts + a broad experience in logic, formal methods and theorem proving. The + Faculty of Mathematics and Computer Science of Eindhoven University of + Technology is strong in computer algebra, theorem proving and applying + Web technology to mathematics. Nijmegen and Eindhoven have a long + history in cooperation on topics related to this FET proposal, notably + type theory, theorem proving and combining various computer + mathematics applications, especially using OpenMath. This cooperation + was mainly taking place between the research groups of Geuvers and + Barendregt in Nijmegen and the research group of Cohen in Eindhoven.

+

The research group of Geuvers and Barendregt is part of the EC + sponsored Thematic Network ``TYPES'' (IST-1999-29001) and of its + ancestor, the EC Working Group ``Types for Proofs and Programs'', + which testifies there interest in theorem proving, especially using + type theory based theorem provers. The FTA project (Fundamental + Theorem of Algebra), started in 1999 and to be finished in 2001, has + as its main goal to formalize (in Coq) a large body of undergraduate + mathematics (algebra and analysis), culminating in a proof of the + fundamental theorem of algebra. The formalization of the mathematics + is now finished and the next step is to make the formalization + accessible and usable by others, preferably through the World Wide + Web.

+

The research group in Nijmegen and the research group of Cohen in + Eindhoven are both part of the EC Working Group Calculemus, which aims + at bridging the gap between different mathematical computer + applications, like computer algebra systems and theorem provers. One + of the vehicles for doing so is the definition of OpenMath as an + intermediate language for the exchange of mathematical objects among + computer applications. + The research group of Cohen is part of the + IST Thematic Network ``OpenMath'' (IST-2000-28719) and its ancestor, + the OpenMath Esprit project ({\tt http://www.openmath.org/}).

+ + + + + + + + + + + diff --git a/helm/mowgli/home/xml/sites/site.dtd b/helm/mowgli/home/xml/sites/site.dtd new file mode 100644 index 000000000..36a40eeb3 --- /dev/null +++ b/helm/mowgli/home/xml/sites/site.dtd @@ -0,0 +1,31 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/mowgli/home/xml/sites/trusted-logic.xml b/helm/mowgli/home/xml/sites/trusted-logic.xml new file mode 100644 index 000000000..c174450ce --- /dev/null +++ b/helm/mowgli/home/xml/sites/trusted-logic.xml @@ -0,0 +1,30 @@ + + + + + + Trusted Logic + France + http://www.trusted-logic.fr +
???
+ + +

Created in January 1999, TRUSTED LOGIC S.A. is a french start-up company, + which presents a unique combination of expertise in embedded + software challenges and in formal methods analysis. + TRUSTED LOGIC offers a wide range of efficient and secure solutions for + smart cards and terminals in the following areas : open systems for smart + cards (Java Card,Windows SmartCards, Multos), open systems for terminals + (mobile phones, PDA, bank terminals, etc), e-commerce, remote secured + access to intranets, and secured networks infrastructures (home or car + control).

+

The development methodology, inside Trusted Logic S.A., includes a + permanent concern of quality and security aspects (formal specification + and proofs) that provides a software which is efficient, reliable and + ready to face high level Common Criteria evaluations when needed

+

The main actors in the smart card and in the embedded software industry + are among its customers : Sun Microsystems Inc., Bull, Gemplus, Oberthur, + Schlumberger, ST Microelectronics, VISA International, Carte Bleue, GIE + Cartes Bancaires, ActivCard, Proton World International, etc.

+ + diff --git a/helm/mowgli/home/xml/work-packages/distribution.xml b/helm/mowgli/home/xml/work-packages/distribution.xml new file mode 100644 index 000000000..9aaa5cf92 --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/distribution.xml @@ -0,0 +1,56 @@ + + + + Distribution + Month 18 + Month 30 + + + + + + + +

Overall architectural design of the distribution model, + its implementation and integration with the consultation + engine.

+ + +

The work is articulated in three, conceptually sequential + tasks:

+
+
T5.1
+
Architectural Design of the Distribution Model. The big + issue it to find the right compromise between two opposite + requirements: distribution (in the sense of the + Web: few rules, no central authority) and coherence + (coherence between different copies of a same document + and global management of the library as a single rational + development). Other architectural problems to be solved + are the management of Uniform Resource Identifiers, their + mapping to Uniform Resource Locators, and the integration + of databases in the distribution model. The final aim is + to have a phisically distributed library with a + single logical view.
+ +
T5.2
+
Prototype implementation. First prototyping implementation + of the distribution layer.
+ +
T5.3
+
Integration with the Consultation Engine. First + implementation of the library as a distributed repository. + Distribution should be completely transparent to users of + the Consultation Engine.
+
+ + + + +

The main milestone is the release of the advanced MOWGLI + prototype, for the fourth meeting of the project, at month + 24. The advanced prototype will integrate the previous one + with the new distribution facilities offered by the + distribution layer.

+ + diff --git a/helm/mowgli/home/xml/work-packages/information-dissemination-and-exploitation.xml b/helm/mowgli/home/xml/work-packages/information-dissemination-and-exploitation.xml new file mode 100644 index 000000000..f67b2dce5 --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/information-dissemination-and-exploitation.xml @@ -0,0 +1,50 @@ + + + + Information Dissemination and Exploitation + Month 3 + Month 30 + + + + + + + +

The work package aims to:

+
    +
  • involve the largest community of professionals in the + modelling phase.
    • +
  • promote dissemination of project results in the relevant + international forums.
    • +
  • promote the use of the service, both for educational and + professional purposes. This phase will start after the + release of the first prototype, at month 18.
    • +
+ + +

The dissemination of results is in charge of the Project + Dissemination & Exploitation Committee, which is + responsible to prepare, during the first six months, a + detailed dissemination work-plan (D2), and to follow its + execution during the Project.

+

Information dissemination will take place via + professional journal articles, presentations at conferences, + international news groups, specific interest groups and so + on. Relevant reports of the projects will be made publicly + available on the World Wide Web. For advanced + releases, we also plan to prepare an ``information pack'', + including a folder and CDROM with demos.

+ + + + Scientific Publications on professional journals + and conference proceedings. + +

Criteria for evaluating MOWGLI's dissemination and its + technological impact will be detailed in the Dissemination + and use Plan. The Project Dissemination & Exploitation + Committee will be in charge to monitor the state of + advancement of the Project according to these criteria.

+ + diff --git a/helm/mowgli/home/xml/work-packages/interfaces.xml b/helm/mowgli/home/xml/work-packages/interfaces.xml new file mode 100644 index 000000000..66acef64b --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/interfaces.xml @@ -0,0 +1,62 @@ + + + + Interfaces + Month 3 + Month 24 + + + + + + + +

This Work-Package is devoted to the design and the + implementation of the interfaces to the library, covering + rendering, browsing, searching and retrieving + functionalities. Some additional functionalities for + authoring purposes (such as computer assisted annotation of + proofs) will be also taken into account.

+

Our privileged rendering language will be MathML, which is + likely to be rapidly adopted as the main language for + representing mathematical notation on the Web.

+ + +

The work is organised in the following tasks:

+
+
T4.1
+
MathML rendering/browsing engines. Our privileged + rendering language will be MathML. In order to be able to + test the presentational stylesheets,(Task 2.5) we need a + MathML compliant browser, that will be developed as a + part of the project (starting from a previous + prototype).
+ +
T4.2
+
Consultation Engine (archiving, searching and retrieving). + The task is devoted to the architectural design and + implementation of the main functionalities for the + consultation and the management of the library.
+ +
T4.3
+
Assisted Annotation. This cover an additional + functionality of the interface, aimed to support the user + in the process of annotating a proof in natural + language.
+ +
T4.4
+
LaTeX-based authoring tool. A tool supporting automatic + generation of Content-MathML from a suitably + (macro-)enriched version of LaTeX.
+
+ + + + + + + +

The main milestone is the release of the first MOWGLI + prototype, at month 18.

+ + diff --git a/helm/mowgli/home/xml/work-packages/metadata.xml b/helm/mowgli/home/xml/work-packages/metadata.xml new file mode 100644 index 000000000..911da289a --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/metadata.xml @@ -0,0 +1,51 @@ + + + + Metadata + Month 6 + Month 21 + + + + + + + +
    +
  • Delineation of the basic intelligence to be considered + for encapsulation in metadata, in order to meet the needs + delineated during Requirement Analysis (WP1).
    • +
  • Definition and Development of a specific Markup Model + in RDF.
    • +
+ + +

The precise definition of metadata and their actual + Markup Model are essential aspects for implementing the + main functionalities of the library, and especially for + archiving, searching and retrieving issues. The work will + be articulated in two main, almost sequential, tasks:

+
+
T3.1
+
Use, meaning and classification. This task, based on the + previous documents D1 and D2, is aimed to provide a + precise definition and classification of all metadata + required for an effective and efficient management of the + library.
+ +
T3.2
+
Modelling. This is devoted to the definition of a precise + markup model. To this aim, we plan to use the Resource + Description Framework of W3C.
+
+ + + + +

The definition of the Metadata model is amain milestone, + since the architectural design and implementation of the + consultation engine (Task 4.2) will be essentially based on + it. Similarly, it is required for Task 2.4 (automatic + extraction of metadata).

+ + diff --git a/helm/mowgli/home/xml/work-packages/project-management.xml b/helm/mowgli/home/xml/work-packages/project-management.xml new file mode 100644 index 000000000..4345b43fa --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/project-management.xml @@ -0,0 +1,65 @@ + + + + Project Management + Month 0 + Month 30 + + + + + + + +
    +
  • General project management and coordination.
    • +
  • Knowledge and skills transfer between consortium + members.
    • +
  • Relation to the European Commission.
    • +
+ + +

The Project management will be assured by the following + relevant roles: a) Project Manager, b) Exploitation manager, + c) Work-package Leaders d)Technical Contributors, and by + the following Project Bodies: a)Project Coordination + Committee (PCC), b) Project Exploitation Board (PEB) and e) + Work-package Teams.

+

The {\bf Project Manager} chairs the PCC. The + mandate of the PCC is to represent the Project, report to + the Commission, monitor overall performance of the project, + ensure accomplishment of the technical objectives, promote + project visibility, promote dissemination of project results + in the relevant international forums, promote acceptance of + project results, administer project resources and monitor + project spending. The {\bf Exploitation Manager} will be + responsible for coordinating dissemination and exploitation + activities undertaken by the Project Exploitation Board + (PEB) in close cooperation with the Project Coordination + Committee (PCC).

+

Information flow within the Project will be ensured by + exchange of internal technical papers, notification of + relevant new publications technologies or standards, and + reports from external meetings. All technical documentation + generated by the project will be exchangeable in electronic + format, according to a set of guidelines to be agreed at + project start-up. The project Manager will enforce + adherence to these guidelines. Only strictly formal + correspondence will be exchanged by ordinary mail and + telefax. Urgent correspondence over e-email will be sent + with a request for explicit acknowledgement.

+

The Coordinating Partner will be responsible to prepare + and maintain a Web page of the project and a CVS repository + (also available via Web).

+ + Cost Statements and Project Reports (month 12, 20, + 30). + + + + + +

Main milestones are the periodic meetings, at month 6, 12, + 20, 24, 30.

+ + diff --git a/helm/mowgli/home/xml/work-packages/requirement-analysis.xml b/helm/mowgli/home/xml/work-packages/requirement-analysis.xml new file mode 100644 index 000000000..82d379fd6 --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/requirement-analysis.xml @@ -0,0 +1,84 @@ + + + + Requirement Analysis + Month 0 + Month 6 + + + + + + + +
    +
  • Definition of the application scenarios.
    • +
  • Precise articulation of all the functionalities required + by the system, and all possible expected interactions + with documents.
    • +
  • Overall requirements of the distribution model of the + library.
    • +
+ + +

The work plan is naturally organised in subtasks according + to the different basic kind of interactions and manipulation + to be considered, namely:

+
+
T1.1
+
Mathematics and the Web. State of the art, standards and + tools.
+ +
T1.2
+
Structured and Formal Mathematics. Delineation and + layering of Semantic Components. Requirements for + the interaction with tools for the automation of formal + reasoning.
+ +
T1.3
+
Metadata. Classification and data mining for content-based + mathematical documents, and key architectural guidelines + for the metadata model.
+ +
T1.4
+
Searching and Retrieving. State of the art, use cases and + application scenarios.
+ +
T1.5
+
Distribution. Distributed document repositories and + peer-to-peer interoperability.
+ +
T1.6
+
Document Authoring. State of the art, use cases and + application scenarios.
+
+

Part of the activity, covering Tasks T1.1-2-6 should be + concluded within the first three months, with the + preliminary report D1.a. The main aim of this phase is + to rapidly reach a good level of inter-operability among the + different sites, by implementing a suitable politic of + knowledge and skills transfer between the members of the + consortium (short visits and/or small thematic workshops, + according to the case).

+

However, some delicate issues, such as Metadata, Searching + and Retrieving and Distribution (Task T1.3-4-5) will + eventually require a deeper analysis (deliverables D1.b and + D1.c).

+

WP1 will be eventually closed during the first meeting of + the Project (month six), when all the reports will be + discussed and approved.

+ + + + + +

The preliminary report D1.a is not a realmilestone: + it should be considered as a first internal draft summarising + the main functionalities required by the system and the basic + intelligence to add to documents, as markup and/or metadata, + to meet these requirements. All these issues will be + eventually detailed in D1.b and D1.c, which are real + Milestones, since the rest of the work will be largely + driven by them.

+ + diff --git a/helm/mowgli/home/xml/work-packages/testing-and-validation.xml b/helm/mowgli/home/xml/work-packages/testing-and-validation.xml new file mode 100644 index 000000000..f9e0d707c --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/testing-and-validation.xml @@ -0,0 +1,52 @@ + + + + Testing and Validation + Month 12 + Month 30 + + + + + + + +

The WP intends to measure the system suitability and + scalability and the satisfaction level of users with the + service.

+ + +

Large scale testing and validation will start after the + release of the first MOWGLI prototype, at month 18. We + shall consider three main validation tests:

+
+
T6.1
+
Education. Full development of a fragment of the library + covering a typical undergraduate course in algebra of + analysis.
+ +
T6.2
+
Certified code. The aim is to be able to present the + formalization and the demonstration of some security + properties related to the code embedded into a smart card. + The presentation must be in a format understandable by + the company in charge of the evaluation of the code and + in accordance with the Common Criteria standard.
+ +
T6.3
+
Electronic Publishing. The aim is to test the LaTeX-based + authoring tool and to demonstrate how an electronic + physics journal benefits from the exploitation of + content markup in journal articles.
+
+ + + + + + +

We expect a lot of feed-back during this phase, that will + be taken into account for the definition of the advanced and + final versions of the MOWGLI prototype.

+ + diff --git a/helm/mowgli/home/xml/work-packages/transformation.xml b/helm/mowgli/home/xml/work-packages/transformation.xml new file mode 100644 index 000000000..1cffe28a3 --- /dev/null +++ b/helm/mowgli/home/xml/work-packages/transformation.xml @@ -0,0 +1,96 @@ + + + + Transformation + Month 0 + Month 21 + + + + + + + +

This work package is devoted to the complex issue of + transforming a low level, content description of mathematics + (understandable by automatic applications for the + mechanization of mathematics) into a human-readable + presentational format. It covers both statements and proofs. + The transformation will be decomposed in a sequence of + intermediate steps, for modularity reasons. All + transformations will be implemented by means of + XSLT-stylesheets. Stylesheets will be simple, modular, and + easily composable. All the transformation process should be + independent from any specific application.

+ + +

The work package is articulated in the following tasks:

+
+
T2.1
+
XML exportation. The task is devoted to the translation + of the standard library of the COQ Proof assistant into a + suitable XML dialect, and to the definition of a low-level + DTD for the terms of the Calculus of Inductive + Construction (the logical system used by COQ).
+ +
T2.2
+
Stylesheets to intermediate representation. + Implementation of a bunch of stylesheets transforming the + low-level logical description of COQ-expressions into a + ``standard'' intermediate, content-level representation + such as MathML content.
+ +
T2.3
+
Proof transformation. Similar to the previous task, but + for proofs. The delicate point, here, is the fact that no + ``standard'' intermediate representation currently exists, + and thus it has to be defined.
+ +
T2.4
+
Automatic extraction of metadata. Relevant metadata such + as list of identifiers in critical positions inside + statements can be automatically extracted from the fully + structured representation of mathematical objects. This + information can then be exploited for searching and + retrieving. The precise list of metadata will be defined + in Work Package 3.
+ +
T2.5
+
Presentational Stylesheets. Implementation of a bunch of + stylesheets transforming the intermediate content + representation into a suitable rendering format (MathML + presentation, HTML, etc.)
+ +
T2.6
+
Automatic Proof Generation in Natural Language. Similar + to the previous task but for proofs. In this case, a fully + automated approach is unlikely to produce really + satisfactory results, and the process should be possibly + integrated with some mechanism for interactive annotation + (see Task 4.3).
+
+ + + + + + + + + +

The exportation module D2.a. is our first + milestone: without a large amount of available documents it + would be impossible to test the transformations. Similarly, + without a precise definition of the intermediate language, + and a large sample of documents in this format (D2c-d) we + cannot start to seriously address the presentational issue. + Note that the intermediate language is the real core of the + whole project.

+

The development of presentational stylesheets also depends + in an essential way on the development of rendering/browsing + engines for the chosen presentational language (in + particular, for MathML).

+

For the end of month 18, we expect to have a first working + prototype of the whole application.

+ + diff --git a/helm/mowgli/home/xsl/consortium.xsl b/helm/mowgli/home/xsl/consortium.xsl new file mode 100644 index 000000000..09ee0d8d4 --- /dev/null +++ b/helm/mowgli/home/xsl/consortium.xsl @@ -0,0 +1,40 @@ + + + + + + + + + + Consortium + + + + + + + + + + +

The Consortium

+

+ The Consortium is made of + + sites: +

+ + + + + diff --git a/helm/mowgli/home/xsl/person.xsl b/helm/mowgli/home/xsl/person.xsl new file mode 100644 index 000000000..8323ecf0e --- /dev/null +++ b/helm/mowgli/home/xsl/person.xsl @@ -0,0 +1,114 @@ + + + + + + + + + + + <xsl:call-template name="qualified-name"> + <xsl:with-param name="qualification" + select="person/qualification"/> + <xsl:with-param name="name" + select="person/name"/> + <xsl:with-param name="surname" + select="person/surname"/> + </xsl:call-template> + + + + + + + + + + + + + + + + + + + + + + + + +

+ + + + + +

+ + +
    + +
    • +     +
+ + +

+ + +

+ e-mail: + + + +

+ +

+ Home Page: + + + +

+ + +

+ Address: + +

+ + +

+ Telephone number: + +

+ + +

Short Curriculum Vitae:

+ + + +

Research Interests:

+ + + +

Selected Publications:

+ + + + + diff --git a/helm/mowgli/home/xsl/project.xsl b/helm/mowgli/home/xsl/project.xsl new file mode 100644 index 000000000..ba1f7a9bd --- /dev/null +++ b/helm/mowgli/home/xsl/project.xsl @@ -0,0 +1,45 @@ + + + + + + + + + + The Project + + + + + + + + + + +

+ + ( + + ) +

+

+ Project type: + + ( + + ) +

+

+ Proposal Contract Number: + +

+

+ Operative Commencement Date: + +

+ + + diff --git a/helm/mowgli/home/xsl/publication.xsl b/helm/mowgli/home/xsl/publication.xsl new file mode 100644 index 000000000..49a9b7b17 --- /dev/null +++ b/helm/mowgli/home/xsl/publication.xsl @@ -0,0 +1,45 @@ + + + + + + + + + + <xsl:value-of select="publication/title"/> + + + + + + + + + + +

+

+ + + + + + + + + + , + + + + + ; + + +

+

+ + + diff --git a/helm/mowgli/home/xsl/site.xsl b/helm/mowgli/home/xsl/site.xsl new file mode 100644 index 000000000..df3ce1d0d --- /dev/null +++ b/helm/mowgli/home/xsl/site.xsl @@ -0,0 +1,83 @@ + + + + + + + + + <xsl:value-of select="site/name"/> + + + + + + + + + + + + +

This is an aggregate site, whose members are:

+ + +
+ + + + + +

+

+

+

Visit the institution home page.

+

+ Site responsible: + + + + . +

+ + +

Projects developed by this site related to MOWGLI:

+ + + + + + + +

+ + + ( + + ) + +

+

Visit the project home page.

+

Members of the project also involved in MOWGLI:

+ + + + + diff --git a/helm/mowgli/home/xsl/work-package.xsl b/helm/mowgli/home/xsl/work-package.xsl new file mode 100644 index 000000000..62231d7b8 --- /dev/null +++ b/helm/mowgli/home/xsl/work-package.xsl @@ -0,0 +1,72 @@ + + + + + + + + + + + <xsl:text>Work Package </xsl:text> + <xsl:value-of select="work-package/@number"/> + <xsl:text>: </xsl:text> + <xsl:value-of select="work-package/name"/> + + + + + + + + + + + +

+ Work Package + + : + +

+

Begin:

+

End:

+ + + + + + + + + + + +
+

Objectives:

+ +

Description:

+ +

Deliverables:

+
    + +
  • + + + + + + + + + + +
    • +     +
+

Milestones and Expected Results:

+ + + +