Mathematics on the Semantic Web

Technical University of Eindhoven.

May 12-14 2003.

Opening	Cohen
Short Presentations	Viglione	How to achieve user-friendly interactivity in mathematical exercises on the Web	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/viglione.pdf) and [HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/viglione.htm)
	Lavirotte	Plan for a mathematical content editor based on SVG display	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/lavirotte.pdf)
	Kohlhase	Towards a Mizar Mathematical Library in OMDoc format	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/kohlhase-mizarinomdoc.pdf)
	Sexton	Glyph recognition for optical mathematical text capture
Invited Lectures	Newhouse	Grid Services	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/newhouse.pdf)
	Nederpelt	Formalizing Mathematics in the Automath Tradition	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/nederpelt/p01.htm)
	Linton	Interfacing with GAP	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/linton.pdf)
MKM	Session Chair: Davenport
	Davenport	MKM Overview
	Dewar	Semantic Markup for Legacy Documents	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/dewar-legacydocs.htm)
	Rioboo	The Foc Project
	Autexier	Management of Change in MAYA	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/autexier.pdf)
	Libbrecht	Authoring semantic mathematical documents with QMath and OQMath	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/libbrecht-authoring/index.htm)
	Libbrecht	ActiveMath: Latest Developments Update	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/libbrecht-activemath/index.htm)
MoWGLI	Session Chair: Asperti
	Sacerdoti Coen	XML encoding and transformation of the Coq library
	Padovani	The GTK Mathview widget	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/padovani.pdf)
	Bertot	Mathematical Interfaces	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/bertot/engltrap.htm)
	Goguadze	Metadata for mathematical documents
CALCULEMUS	Session Chair: Benzmüller
	Benzmüller	The CALCULEMUS Network — A brief Introduction	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/benzmueller.pdf)
	Cohen / Sorge	Groups and Certificates	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/sorge.pdf)
	Trybulec	The evolution of the Mizar Mathematical Library	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/trybulec.pdf)
	Zimmer	The MathWeb Software Bus and Theorem Proving Services
TYPES	Session Chair: Geuvers
	Geuvers	The use of types to formalize mathematics
	Luo	The type-theoretic approach to mathematical vernacular	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/luo.htm)
	Bertot	Types for Proofs, Computers and Mathematics	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/bertot.pdf)
	Ballarin	Isabelle/Isar: formal, yet human-readable proof documents	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/ballarin.pdf)
MONET	Session Chair: Dewar
	Dewar	The MONET Project	[HTML](/https://openmath.org/meetings/eindhoven2003/proceedings/dewar-monet.htm)
	Chicha / Gaëtano	Putting Bernina on the Web	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/chicha.pdf)
	Caprotti	The Mathematical Service Description Language
	Horrocks	OWL: an Ontology Language for the Semantic Web	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/horrocks.pdf)
OpenMath	Session Chair: Cohen
	Hagen	XML, TeX and Math
	Reinaldo Barreiro	Context in Interactive Mathematical Documents
	Kohlhase	Towards OpenMath version 2	[PDF](/https://openmath.org/meetings/eindhoven2003/proceedings/kohlhase-openmath2.pdf)