Towards Community of Practice Support for Interactive Mathematical Authoring

  • user warning: Table './jem/sessions' is marked as crashed and should be repaired query: SELECT COUNT(sid) AS count FROM sessions WHERE timestamp >= 1231452795 AND uid = 0 in /var/www/net.jem-thematic/site/includes/database.mysql.inc on line 174.
  • user warning: Table './jem/sessions' is marked as crashed and should be repaired query: SELECT DISTINCT u.uid, u.name, s.timestamp FROM users u INNER JOIN sessions s ON u.uid = s.uid WHERE s.timestamp >= 1231452795 AND s.uid > 0 ORDER BY s.timestamp DESC in /var/www/net.jem-thematic/site/includes/database.mysql.inc on line 174.

In order to foster the use of proof assistance systems, we integrated the proof assistance system OMEGA with the standard scientific text-editor TEXMACS using the mediator PLATO. We aim at a document-centric approach to formalizing and verifying mathematics and software. Assisted by the proof assistance system, the author writes her document entirely inside the text-editor in a language she is used to, that is a mixture of natural language and formulas in LATEX style. We developed a basic mechanism that allows the author to define her own notation inside a document in a natural way, and use it to parse the formulas written by the author as well as to render the formulas generated by the proof assistance system. This paper examines how the mediator PLATO can be extended to identify, analyze and support communities of practice based on the notation practice of individual authors.

Author(s): 
Marc Wagner (Universität des Saarlands) and Christine Müller (Jacu)
Publication_details: 
SCOOP Workshop: 1st Workshop on Scientific Communities of Practice, Jacobs University Bremen, Germany
Date: 
2007/08/30
Partner_node: 
Jacobs University
AttachmentSize
plato_MWagner.pdf321.65 KB