Authors: Iris Loeb, Lionel Elie Mamane, Herman Geuvers
Title: Interactive algebra course with formalised proofs and definitions
Abstract: 
To enable interoperability and intelligent searching, web-documents require a
semantical mark-up. For readability, however, a nice presentation and hence a
presentational mark-up is needed. With this in mind, we have replaced the
proofs and definitions of a chapter of existing interactive algebra course
notes (IDA by Cohen, Cuypers and Sterk) by their formal counterparts, that we
had first formalised in the proof assistant Coq. To this end we have used and
extended technology for the creation and maintenance of a virtual,
distributed, hypertextual library of formal mathematical knowledge (HELM).
This research is part of the MoWGLI project.