MoWGLI: Mathematics on the Web: Get It by Logic and Interfaces

Katholieke Universiteit Nijmegen

The Netherlands

Subfaculteit Informatica, Faculteit Natuurwetenschappen, Wiskunde en Informatica, Katholieke Universiteit Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands

Visit the institution home page.

Site responsible: Prof. Herman Geuvers.

Site members:

• Prof. Herman Geuvers
• Prof. Arjeh Cohen
• Prof. Henk Barendregt
• Dr. Freek Wiedijk
• Ernesto Reinaldo Barreiro
• Luís Cruz-Filipe
• Milad Niqui
• Jasper Stein
• Dan Synek

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 (see http://www.openmath.org/).

This page is hosted by the Department of Computer Science, University of Bologna. Last updated Fri Feb 2 17:12:19 CET 2007.