Towards Community of Practice Support for Interactive Mathematical Authoring
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.
| Anhang | Größe |
|---|---|
| plato_MWagner.pdf | 321.65 KB |

