“KWARC was!”

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)

Jonathan Fine focuses on capturing and improving large amounts of materials.

MathTran is a public web service and samples. Display on webpage is based on img tags and Javascript. Instant Previews. Coping with the breadth; instead of doing much with little amounts of content (breadth).

See paper

See MathUI submission

At CICM 2008 (Workshop DML), Stephen Watt presented his work on analyzing the frequency of symbols, that would be an interesting infrastructure for further cop-based analysis.
See Michael’s blog and the DML Proceedings.

Another talk (Workshop MathUI) was on his handwriting recognition of mathematical notations: Presenting his Representation Approach. See paper

The challenge is that there is no fixed dictionary. But maybe CoPs provide some restrictions of potential parsing results? Or is frequency a better approach?

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

I’ve never liked blogging, but as I’m now staying abroad for half a year (at DERI Galway), I found it a good way to keep in touch with my friends and fellow researchers. My private blog mainly contains experiences not related to research, but there is also a category “work”. Anything that is too general to be reported here can be found in that blog.

In November 2007, I ask the members of the KWARC group to fill out questionnaires to get a better intuition about the social and scientific practice of the KWARC community. The detailed results have not been published due to data privacy issues, but the general findings are provided in evaluation.pdf.

After reading the book How to solve it by Polya [Pol73], I decided to analyze different ways of problem solving based on how my colleagues and students (altogether 10 volunteers) proved the following simple lemmas: (1) For all prime numbers p≥5 prove that z=p2-1 is divisible by 24 and (2) Proof that the center of gravity of a polygon equals the average of all points of the polygon. Although no representative survey was carried out, the case study brought up some interesting findings: For (1), some person wrote a lot of explanatory text for almost every step of their proof; while others skipped several steps they found obvious. The level of formality varied among the test persons: some wrote their proofs very close to a form that could be verified by e.g. theorem provers, while others stick to a rather informal writing of their proofs. Moreover, the test persons took different approaches of how to proof the lemma: Some could easily write down a formal proof, while others started with examples and counter examples to get a better idea of how to solve the given problem. For (2), some test persons used drawings to get a better idea whether they had to proof or refute the given geometric problem.

I started reading “Gödel, Escher, Bach” and I came across an use case for change management. The author introduces an example on page x. He then starts a new section and discusses a new thought. One the next page (x+1) he refers back to the example (on page x) with the lines “as shown above”. I found that distracting, since the example was on the previous page and I had to interrupt my reading to make sense of this line.

I am guessing, the author had a different format when writing the book. There, the example most likely was on the right page and his reference made absolute sense. But depending on the format we choose for printing/ displaying a document, references need to be adapted. In consequence, change management is also useful for automatically updating references inside of documents. Although, I guess, these do not need to be propagated and, therefore, are not that exiting :0)

By the way, I would really like that feature when writing papers: I often leave out the caption of figures to save room. Hence I must use references such as “to the left” and need to update these references whenever I rearrange a picture.

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.”