We describe a case-study of the application of web-technology (HELM) to create web-based didactic material out of a repository of formal mathematics (CCoRN), using the structure of an existing course (IDA). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the ``view''), and the rendering of proofs.
Asperti, A., Geuvers, H., Loeb, I., Mamane, L.E., SACERDOTI COEN, C. (2006). An Interactive Algebra Course with Formalised Proofs and Definitions. s.l : Springer.
An Interactive Algebra Course with Formalised Proofs and Definitions
ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO
2006
Abstract
We describe a case-study of the application of web-technology (HELM) to create web-based didactic material out of a repository of formal mathematics (CCoRN), using the structure of an existing course (IDA). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the ``view''), and the rendering of proofs.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
