“KWARC was!”

There are multiple solution to a mathematical exercise:

• 8 ways for Three by One
• Different numbers of proving steps: see MKM: Specifying Strategies of Exercises

Very interesting approach. They take our notation-rendering approach on the level of documents, i.e. presentation markup is interpret wider and includes narrative presentation markup:

Plain text documents are first structured and verified; missing proof steps are propagated to the initial document and, in particular, “rendered” into the “plain text presentation”.

For CoPs it would be interesting to analyze different proofs wrt. the level of detail.

See MKM Proceedings: Authoring verified documents by interactive proof construction and verification in Text-Editors. (Dominik Dietrich, Ewaryst Schulz, Marc Wagner)

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

Description in the CAPS 2008 call: “Proactive systems need to be able to understand the different contexts that apply in and for any given user/communication situation. Such context awareness is based on inference of sensor data to achieve knowledge on a users’ state, emotions, activities, goals, etc. and to proactively adjust the systems behavior. Deploying proactive systems in the increasingly embedded and ubiquitous environments further raises the need to make them context-aware.”