Marc Wagner implemented a plugin for TeXmacs which tracks a user writing and modifying a document. This was done to gain intuitions for extending is Plato editor (identifying the linguistic phenomena). And interesting aspect are that the process of writing of notations is also a practice, not just the selection of a notation. Another aspect is the level of formality users choose to solve their tasks. An analysis of the solutions might be an interesting case study for CoPs.
- Most modification where due to notations errors (so automatic verification would be very helpful).
- Sentences fragments where classified (linguistic ontology to deal with linguistic proofs)
- Pointed out practice for “concluding step”.
- Pointed out practice for “justifying” steps. (partly very hard to parse automatically: specific science or natural language)
Plan for the future: Additional components for the “ideal mathematical assistance system”. Among others
- Linguistic Ontology for concepts, types, theory structures.
- Dynamic Adaptation of Notations (Change Management).
- Context Memory???.
See paper at MathUI 2008