Cory Casanave, a participant of today’s Ontolog conference call mentioned a versioning ontology, as versioning (of data and metadata!) was identified as an important feature of semantic wikis.
Here is their ontology for versioning and management of change; somewhat different from our group’s notion of management of change, though.
Hypotheses: Mathematical Software needs MoC (well at least that was what I was going to show)
Evidence: I am referring to software that helps finding a proof, that supports the iterative process of adding proving steps and deleting them again, that is the tedious process of slowly approaching the proof in a notation one is satisfied with. I am not referring to theorem provers that proof lemma’s for us and fill in correct steps automatically nor to tools that help digitalizing already known or written proofs. The continuous revision and multiple revision require a permanent adaptation of previous written proofs steps, thus, respective software with management of change support is valuable for mathematicians.
Another feature: The tedious proving process is very different to the final proof or the later presentation of the process to other (in publications, books, slides, and even in discussions with other mathematicians). Thus, for reconstructing the actual proving process, the software can offer recording functionalities. This could be used by others (in particular students) to better understand the methodology of finding a proof and the heuristics used to require the proof (well, we can’t look in the mathematicians head; some iterations made not be entered but rather take place in the human mind or using pen and paper).
Revision/ Concerns: However, do mathematicians really want such a tool? It would be tedious to enter notations (and particularly to decide on a notation, thus, slowing down the actually thinking) and most likely mathematicians rather stick to their heads and paper. So we should rather ask: When do mathematicians use software? Where can software potentially ease up their life? Is this maybe rather after the finding of a proof; when it comes to the point the mathematicians want to share it with others, publish it; verify it (automatically)? So then we would not need software that supports the tedious, iterative phase of finding proofs … but rather software that supports the publication process (still then change management is useful, since notations/ text evolve – also when writing down an already completed proof) — and the learning experience (since young mathematicians need to learn how to proof).
So does learning software in mathematics make sense? Can it potentially ease up the learning experience? What can software do better/ more efficient/ and less costly then human specialists?
A final though: Mathematicians tend to collaborate to solve proofs (really?). And with the growing globalization, they can refer to modern technology to find potential collaborators and to communicate (do they?). Software can indeed be useful to provide the respective search facilities; communication channels; and digital working spaces (including change management). Software can thus influence and change mathematical practice by opening new spaces to do math (potentially interesting for particular young mathematicians).
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.
Subversion, CVS, and many other version control systems use a copy-modify-merge versioning model. In this model, each user’s client contacts the project repository and creates a personal working copy. Users then work simultaneously and independently, modifying their private copies. Finally, the private copies are merged together into a new, final version. The version control system often assists with the merging, but ultimately a human being is responsible for making it happen correctly. In particular, if changes of one author overlap with changes of another one. This situation is called a conflict. A common believe is that software can’t automatically resolve conflicts; only humans are capable of understanding and making the necessary intelligent choices. Henceforth I call this the conflict resolution paradigm.
However, I don’t agree on this commonly accepted paradigm! Instead, I propose using structural semantic techniques in conjunction w/ equality theory allows for offering semi-automated management of change to increase machine readability and understanding, respectively, and thus to decrease costs of manually resolving conflicts!
Structural semantics enables the computation of dependencies and thus the computation of long-range effects of changes. That is, local changes respecting dependency relations can be automatically propagated and adapted. Equality theory, on the other hand, enables to reduce conflicts at all, in a sense, where are no changes there could be no conflicts. That is, changes respecting equivalence relations are no changes in this sense and do not have to be propagated and merged, respectively.
So, eventually to reduce conflicts in and ease collaborative work-flow processes we have to clarify (on the conceptual level) and formalize (on the technical level) the conceptualities “dependency”, “dependency types”, “change types”, and “propagation” w.r.t. respective equality theories. In my PhD thesis I am currently working on both the conceptual and technical level to end up w/ a general management of change methodology. As a proof of concept in the application area of collaborative authoring processes I use my prototype system locutor.
/nm
Transfered from Sundries of Anything posted by Jochem Liem
I met Normen during the poster session at KI2006 while he was explaining Christine about his research. Basically, he uses a structured markup language (in this case LaTeX) to describe the “logical” structure of parts of the document (called infoms).
Currently, an ontology about types of infoms and their relations developed in a European project is used, but custom ontologies can be used to structure documents.
Structuring the document using the infom types defined in the ontology should allow versioning as the changes to infoms (and their relations to other infoms) are formally defined.
I did not really understand why the killer application for structured documents would be versioning, and argued that there are other applications which seem at least as sexy.
1. Collaboration. The infoms could describe the flow of an argument. When writing papers together, the changed infoms could be highlighted. Metadata (data about the changes) could be added to describe why the infom was changed. This seems like something which would be extremely handy to use. Because you structure your content using infoms, the purpose of specific parts of text is also made explicit. This makes it far easier for co-authors to understand the reasoning of the author. Collaboration is a topic which fits in the AIED conference series.
2. Text analysis, suggesting improvements. If the structure of a document in terms of content is known, it is probably possible to say something about the flow of the document. For example, if support for a statement is extremely far away of the statement itself, the document probably has to be restructured. If the knowledge about the document is good, you might even suggest where certain infoms have to be placed.
3. Text editing on a meta-level. It might be possible for a perfectly annotated document to be restructured. For example, the text could be visualised using boxes for the infoms, en arrows for the relations between them. Changing the infoms on the screen also changes their position in the document. This way the flow of a document (an argumentation for example) can be changed on a meta-level. Visualising these relations makes it intuitive for the user whether his new flow of infoms makes sense.
Somehow, I think this kind of research also fits in the semantic web vision. By structuring documents you might be able to make them machine accessible. Currently, it is not clear how text-documents and ontologies should be integrated. We have markup languages like XHTML for text and ontology languages like OWL for concepts, but they each serve a different purpose. So, how do we use the semantic web accomplishments to annotate text document in such a way they can be used by semantic search/service discovery/brokering/etc?
Solving these problems is probably worth multiple PhD’s. Normen, from what I’ve written, have I understood what you are working on? Also, please let us know when we can use your work. ;P
I must confess that I’m still using locutor and Subversion in parallel. While that could mean that I do not entirely trust locutor, it also opens my eyes for little differences between both systems. For example, I requested a status report of a working copy, both with Subversion and with locutor:
~/svn/kwarc.eecs/www/projects/swim$ svn st
A images/swim-0.1.png
M index.xml
A download
A download/swim-0.1-bin.zip
A download/swim-0.1-bin.tar.gz
~/svn/kwarc.eecs/www/projects/swim$ loc st
A download
A download/swim-0.1-bin.tar.gz
A download/swim-0.1-bin.zip
A images/swim-0.1.png
M index.xml
I like locutor’s order (first subdirectories, then files) much better, as files in the current directory can easily be overlooked in Subversion’s summary.
Being used to Subversion’s command-line client svn, I don’t want to always type locutor on the command line. Therefore, I created an alias in my shell configuration (e.g. ~/.bashrc):
alias loc=locutor
This assumes that locutor is in the PATH. In my case, I have a directory ~/tools/locutor in the PATH, which is a symbolic link to ~/tools/locutor-<version>. That makes it easier to install new versions and, just in case they should be buggy (which so far has never occurred to me 
), switch back to an older version.
I’ve been using locutor around the clock during the last four days of our EU proposal. Well, to be honest, that almost drove our coordinator crazy and, looking back, I do have to admit that it was quite risky to use a young system like locutor when every second counts. Especially, since after installing locutor my SVN version was out-of-date and I couldn’t easily switch back to it.
Nevertheless, besides to little bugs (which will be fixed in the next version), I did not experience any difficulties using the new system. From the installation until the last commit of the proposal, locutor has been working smoothly and reliable. I am looking forward to try out more features. So – keep it coming :0)
~Christine