This description of the Music Ontology provides an excellent and easy to understand example of how existing ontologies were reused, and other small ontologies designed, to contribute to the development of a larger, integrated ontology.  A similar case as in our current development of a versioning ontology for OMDoc, which we are specifying at the moment and which will be made up of a versioning ontology, a change ontology, an event ontology (the one that is part of the music ontology), and an ontology for people.

I’m currently reconsidering whether it was a good idea to implement my XML→RDF extraction library Krextor in XSLT. Writing down my actual requirements, I realized that I need a language that supports

• pattern matching on XML elements and attributes, using a syntax that is close to literal XML or to XPath (for easily writing extraction rules, which should also be done by other developers in future)
• functional programming (in some way), as the whole idea of mapping XML to RDF (and thus XML nodes to URIs) can be modeled most elegantly using a functional approach. (This is rather a requirement for me implementing the generic core of Krextor, but also for extraction module developers once the XML input language is a bit more complex.)

Having looked a bit into XQuery, Scala, and JavaScript (and a little bit into Haskell), I decided to stick to XSLT for now. Functional programming is awkward but possible, and XML pattern matching is awkward or non-intuitive in most other languages.

Cristian Calude and I discussed the price and gains of content mark-up. He emphasized that unless we provide interesting features, mathematicians will not see the value in content mark-up and the reason for additional efforts (e.g. when using sTeX instead of LaTeX).

Below you find three groups of mathematician that most likely need different amount of arguments to be convinced (please note that I am not citing Cris. I simply present what I remember from our discussion and made up the names of the groups):

• Pen-and-Paper guys: They only use computers for publishing but all mathematics is actual developed on paper. The publishing process is seen as a tedious and inconvenient activity that takes time away from the actual job that a mathematicians wants to do. The digitalization is annoying (proof reading). In earlier times, this was done by secretaries and the publisher, but nowadays publishers only accept LaTeX, which is really seen as a burden by this group of mathematician.
• LaTeX Lovers: There are mathematicians that think in LaTeX. The use it a lot for developing their ideas and incrementally revising proofs with colleagues. This groups seems to have an increasing influence on scientific publishing as most publisher (in mathematics) will nowadays reject a submission if it is not provided in LaTeX.
• Innovators: The third group wants even more. (We didn’t really talk about this group long) For example, this groups promotes semantic technologies and aims at making mathematics machine-processable as well as bringing mathematics to the web. I assume that includes vast parts of the MKM community.

Maybe we need to start asking ourselves: Would we use our tools and services? (Who is using sTeX?) And if so, for which activities? Think of the very early steps towards a new topic. Would you like to be forced to content mark-up? Although we provide full flexibility in switching between concepts, simply having to establish theories and marking up structure really slows down the creative thinking. So when is a good timing of using content-based techniques? Do we restrict it to the very last stage of scientific work, i.e. the publishing process, or teaching (the latter not even recognized as scientific activity)?

I am collecting arguments on gains and burdens of content mark-up (in the panta rhei trac), in particular, with a focus on the technologies and services provided by KWARC. I’d appreciate your feedback and comments!

A considerable part of the implementation of my research prototype(s) is done in XSLT. Now that the extraction of RDF from semantic markup is more and more turning in to a project of its own, more software engineering was needed – including proper documentation.

It turned out that XSLTdoc is a really nice solution for that: Just put a few additional XML elements in front of every template or function and run a special XSLT to generate the documentation. Works like javadoc and looks nice.

I recently read an interesting paper that was presented at the INSEMTIVE workshop (incentives for the semantic web). Hans-Jörg Happel addresses the problem that a lot of metadata (tags, annotations, etc.) exist in private knowledge spaces but are not shared on the semantic web – maybe because of privacy concerns, maybe because nobody has ever asked for them, whatever. His new idea is to design a search engine that knows which private metadata could improve the result set – and then asks their authors to publish them: i.e. the opposite of the “publish first, retrieve then” process of traditional IR.

• paper
• slides

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.

My third meeting with Cris …

• The Way of Discovery Math: Cris highlighted again that it is important to distinguish the following two aspects in mathematics, i.e. presenting mathematical results and actually discovering mathematical results. He said, if I want to really understand mathematical practice, I need to follow and analyse the second aspect. In his lectures, Cris is trying to teach his students how to discover math, but this is indeed difficult, he says. For example, he is intentionally presenting them several wrong definitions before finally concluding with the correct definition. Even in one of his paper, Cris et al. successfully published several wrong definitions (before introducing the correct one) of a non-deterministic automata, although the reviewers first wanted them to “remove the rubbish”: C. S. Calude, Elena Calude, B. Khoussainov. Finite nondeterministic automata: Simulation and minimality, Theoret. Comput. Sci. 242, 1-2 (2000), 219-235. He also pointed me to the books of George Polyá, in particular, Mathematics and Plausible Reasoning. Further Cris said that if we train (young) researchers we have to teach them “to have the guts to not be afraid to be wrong“. And then he said: “The productivity of a PhD is 5%, 95% is failure” and this is almost the same situation for professional mathematicians (besides some genius), who do not continuously produce correct and beauty proofs and theorems.
• An assessment system for mathematical knowledge: Cris said that my proposal is still to vague and abstract to be understood by other scientists. He made an example to illustrate that I should work on my presentation of new ideas (freely cited, not his actual words): “When I present my view to solve a mathematical problem I need to include to things: (1) I need to provide a number of concrete steps towards the solution, i.e. first I proof this, then I proof this, … and I have to point to the basic methods I will be using, e.g. I’ll use graph theory rather then topology. (2) I need to point to my previous accomplishments, i.e. some steps I have already addressed. Then people will accept it more likely.” Cris also said, that for the existing achievements, I do not necessarily have to provide my own work, but I can point to existing research and that will increase my acceptance. So what I will do for my seminar talk is, to put more emphasis on the methods and related work part. And I will use many examples to illustrate my approach. I will have a look at Cris GoogleTalk again. However, in general, Cris thinks that this could be interesting. Actually he believes that 90% of all published mathematical proofs are either incorrect, incomplete, or uninteresting. “Having over 100.000 published a year, how are can you still find your way without any guidance? You have the expertise in your small community, but as soon as you have to rely on work outside your field, you have to trust the expert.“

I also met interesting people today, I am eager to talk to further. And I’ll get a chance tomorrow, as there is the “end of the lecture party”.

• Emilia Mendes expert is web development.
• André Nies mathematician
• Brian Carpenter (haven’t met him, but will soon). Cris recommended me to read his A Dialogue on the Internet, published in Bulletin of the European Association for Theoretical Computer Science (2008)

Gathering Information on this community as well as the current state-of-the-art in research and industry.

There are several events for the user modelling and adaptation community. However, both are closely related, which one can also see by the recent merge of two of the biggest venues UM and AH. I was told that besides the venues on international ground, ABIS is an important meeting on a national layer (The workshop has solely taken place in Germany, but gathers researchers across Europe).

• ABIS Workshop (Satellite event of the LWA Workshop)
• International Workshop on Semantic Media Adaptation and Personalization (2008)
• International Conference on Intelligent User Interfaces
• International ACM Conference on Recommender Systems
• Artificial Intelligence in Education (CfP 2009)
• User Modeling Inc. (check out more related conference, job postings, and research groups)
• Conference on Adaptive Hypermedia and Adaptive Web-Based Systems: All forms of Web and Hypermedia personalization from personalized search and browsing to recommender systems to personalized E-Learning. (2008)
• International Conference on User Modelling (2007)
• 1st and 7th International Conference on user modelling, adaptation, and personalization (2009): User Modeling (UM, 1986-2007) and Adaptive Hypermedia and Adaptive Web-Based Systems (AH, 2000-2008) have been merged into the annual conference series User Modeling, Adaptation, and Personalization (UMAP)

Subscribe to more news: Mailinglist by TUE

• Amazon: Adaptive Hypermedia in eBusiness: Recommendations based on user preferences and prior history
• For further professional approaches see keynote by Alexandros Paramythis

• Adaptive Hypermedia (AH) tailors what the user sees to the learner’s goals, abilities, interests, knowledge, etc. [..] offers a selection of links or content most appropriate to the current user (in his current context, whereas context refers to the device). “Adaptive hypermedia is closely related to Web personalization.”
• Adaptive Educational Hypermedia: “Fundamental problem is that learners inevitably have diverse backgrounds, abilities and motivation – and hence highly individual learning requirements.” (AC 2005) Doesn’t target stand-alone systems (unlike intelligent tutoring systems), but hypermedia systems.
• Distinction between adaptation ((automatic) system-driven personalisation and modifications) and adaptability (user-driven personalisation and modifications).
• The Adaptive Web: Methods and Strategies of Web Personalization (Book by Peter Brusilovsky, 2007)
• AHA Project funded by the NLnet Foundation (1997 - up to date): see The Design of AHA

Looking at the work in the area of adaptive hypermedia, I believe, that ours and their work go well together: We have a strong representation format of mathematical knowledge (focusing on the design so far and slowly moving to ways of manipulating it, see e.g. JOMDoc/ JOBAD), while they have placed good thoughts on the user modelling, strategies for adaptation, and general frameworks for designing adaptive systems.

The motivation and focus of AH, seems to overlap with our work (cf. Peter Brusilovsky; AHA Project; Alexandra Cristea): For example, to improve accessibility of mathematical knowledge, we talk of adapting it, in particular by selecting, sequencing, and presenting mathematical knowledge for a user or community of users.

• Problems with hypermedia applications: (1) Navigational freedom: which links are relevant (for this user)?; (2) Comprehension: what has the user seen before when reaching a certain node? (3) Presentation: what fits the user’s screen? how much network bandwidth and processing power is available? (cf. Talk)
• Opportunities with AH: (1) Guide users towards relevant information (users can reach relevant information more easily and more quickly), (2) Make sure users can understand the presented information, (3) Change the presentation so that it fits the user’s platform and environment (cf. Talk)

If we look at the layers of the LAOS framework (cf. AC 2004), we can see a great overlap to the OMDoc approach. I believe we are much stronger on the content representation, while OMDoc is still missing the user modelling and adaptive layer:

1. Domain model (DM) containing a collection of linked resources
2. Goal and constraints model (GM) containing goal-related information, such as instructional and pedagogic information about the resources
3. User model (UM) containing user-related information, such as information about the learner
4. Adaptation model (AM) containing the behaviour and dynamics, such as, a learning style related adaptive strategy
5. Presentation model (PM) containing display and machine-related information, such as the foreground-background colour scheme for the course presentation

In order to make OMDoc (systems) adaptable/ adaptive, we need to provide these layers: (1) OMDoc Commons interlinked on different layers, i.e. logical, narrative, rhetorical, argumentative (?); (2) theory morphisms, i.e. mathematical/ logical prerequisites but maybe also rhetorical prerequisites; (3) is missing; (4) is missing; (5) presentation-pipeline.

I have the feeling that the challenge of bringing mathematicians and computers closer together, requires a lot of expertise in the field of pure mathematics and the more technical-field of mathematical knowledge management. The latter requires a good overview on mathematical tools, in particular, computer algebra systems and theorem provers as well as other mathematical editors (e.g. Plato). Moreover, the step-wise formalization of mathematical text seems to be a core interest and competence of the whole KWARC group rather then my own research focus.

Looking at the discussion with Cris on the confidence in proofs, acceptance of proofs as well as trust in proofs, I am wondering, whether we could use our understanding of the mathematical practice and use it for providing an assessment and reputation system for mathematics, i.e. something that we could attach onto a repository of mathematical knowledge and use to facilitate the collaboratively assessment of the mathematical community on different layers:

• Is (the proof) published in journals (considering the impact factor of these journals)
• Was it accepted by the Zentralblatt or Mathematical Reviews (adding more confidence)?
• How long was the proof tested by the mathematical community?
• How many proofs do exist for the theorem?
• Is it a nice proof/ theorem (beauty)?
• Is it correct? (later adding automatic verification methods …)
• Can it be understood (e.g. measured by the numbers of references and re-uses)? How hard can it be understood?
• Is it re-used by the community, i.e. is it relevant and useful for further mathematical work?

We can imagine a top-down and bottom-up approach:

1. The top down approach requires the user’s explicit assessment of the content: evaluating the users’ ratings, tags, bookmarks
2. The bottom up approach could implicitly provide the relevance of content making use of the logical and narrative structure of the mathematical knowledge: computing theory interrelations, citations, …

I will discuss with Cris, whether he thinks that this would lead to a useful application for mathematicians.

Communities of Practice in Mathematics
Christine Müller is a PhD student from the Jacobs University Bremen, who is working with Prof. Cristian Calude for the next 7 months. In her PhD, Christine is using the metaphor of Communities of Practice to enrich semantic mark-up formats for science, in particular, mathematics with social and collaborative components. By integrating social (Web2.0) technologies and user modelling techniques, Christine aims at eventually improving the management, in particular, the accessibility of mathematical online materials. To illustrate and evaluate her approach, she is currently implementing a prototype eLearning application, which is used within an introductory Computer Science lecture at Jacobs University Bremen.

In the seminar, Christine will introduce the underlying representation format for mathematics and present the latest findings of her work, i.e. a framework for the context-aware adaptation of mathematical notations.

Please note, I am currently in the progress of structuring and narrowing down my research interest.

Communities of Practice: Using the metaphor for all the subsequent research interests …

• e.g. for extending document mark-up formats with social and collaborative components
• e.g. for understanding mathematical practice
• e.g. for the discussion on adaptation/ user modelling/ community modelling

Document Management

• Semantic mark-up of mathematical documents and mathematical practice
• Logical structure of mathematical knowledge (theories and interrelations)
• Narrative (didactic/ rhetorical) structure of mathematical documents (see mathui paper)
• Mark-up of mathematical notations and notation context (see small survey, see mathui paper, mkm 2008)

Accessibility of Mathematical Knowledge

• Adaptation of mathematical knowledge: Selection, Sequencing, and Presentation of mathematical knowledge (see ABIS, FGWM)
• Adaptation of mathematical notations
• Intelligent selection and recommendation of mathematical examples and exercises
• User modelling and community modelling (see ABIS, FGWM)

Semantic Packaging Format: Integrating Semantic Tools (WSKS paper)

Integrating Semantic Web and Social Web

• Enriching (semantically marked-up) mathematical documents with social contexts: ratings, semantic tagging
• Discussion and social interaction with (semantically enriched) mathematical contents

Case study: proof-of-concept prototype for mathematical E-Learning

My second meeting with Cristian Calude has clarified some of the issues from the first meeting …
Please note that Cris does not necessarily share my personal opinions and summaries on this page.

• Confidence in and Acceptance of proofs: In the previous meeting, I haven’t be sure about what Cris means with context. Cris means by this, that the confidence in a theorem increases by the number of applications, i.e. the number of times it is reused by others e.g. to prove another theorem. This application can be interpreted in two ways: (1) Other mathematicians understood the prove and (2) the mathematical community assessed this contribution to be relevant. In particular, Cris again pointed out that there a several dimensions of a accepted and significant theorem: Neither beauty nor correctness are enough, but it also has to be understood and used by the community, i.e. it needs to be relevant and useful for further mathematical work.
• Reusing trusted and correct Theorems: Cris illustrated today how critical it is to reuse only trusted and correct theorems and that even then mathematicians have no certainty as there is no absolute correctness: In 1988, Yoichi Miyaoka, number theorist at the Max Planck Institute in Bonn, claimed that he had proven the Fermat’s Theorem (eventually proved by A. Wiles). As I was told, his actual proof was not the direct flaw, but when checking his proof step-by-step, the professional referees identified that one of the theorems he re-used was incorrect. However, that theorem had been published and reused by other mathematicians, but had not been carefully checked so far (cf. NY Time). This is a phenomena I have heard before, i.e. sometimes proofs without central interest to the community are not extensively checked.
• Mathematics and Computers: As far as I understood, Cris is interested in integrating traditional and unconventional mathematics, i.e. axiomatic-deductive thinking and computer-supported experimenting to finally achieve a proof. He believes that mathematical proofs will more and more be checked by computers. Of course, this will be a gradual process, from solely human referees to fully automatized proof checking. In our last meeting, we identified to ways of addressing the problem of bringing mathematicians and computers closer together: (1) less formal and human-friendly systems and (2) new ways (of thinking and the respective tools) for encoding mathematical knowledge. Cris is envisioning a process that will support authors to convert their proofs (consisting of text and formulae) to fully formal formats that can be object of automatic provers. In a first step, he would like to see that we can distinguish pure comments from text that is part of the proof. This would require tools and a respective representation format for mathematical documents: The tools need to (semi-)automatize the annotation of mathematical text. Different technologies can be of use from natural language parsing to semi-automated semantic annotation ideally integrated in the publication processes of mathematicians (see sTeX as semantic extension for LaTeX; invasive editors for MS PPT and Word; Sentido; and SWiM). The format has to support the mark-up of narrative, rhetorical, but also mathematical concepts (see OMDoc and its extension in the 2.0 version). However, apart from the format and tools, Cris vision also includes a social aspect that has to evolve over time, i.e. mathematicians have to trust in computer-checked proofs and they actually have to use the tools for formalizing their documents and this leads us to an ongoing-discussion, also referred to as authoring-dilemma (see Andrea’s work).
• Collaboration with Cris: Potentially, Cris and I will work on a programmatic paper of what one should do to help integrating traditional and new mathematical practice, i.e. to motivate our this vision and to give concrete suggestion on how to realize it step by step. However, in a next meeting I will introduce him to my work and areas I am involved in, from there on we will make further decision. I will also give a seminar talk here in some weeks to introduce my work to the CS/ math department.

Notes on Cristian S. Calude et al. (2007) Proving and Programming (see also previous post, see slides). Please note that the authors do not necessarily share my personal opinions and summaries on this page.

There is a strong analogy between proving theorems in mathematics and writing programs in computer science. Programming gives mathematics a new form of understanding. The computer is the driving force behind these changes.

• “Theorems (in mathematics) correspond to algorithms and not programs (in computer science)”
• “Programs (in computer science) correspond to mathematical models.”
• Proving the correctness of algorithms is seldom a focus in software projects (but: even testing/ documenting is sometimes neglected)
• Do some programming language facilitate/ required to put more focus on the correctness of the algorithms (e.g. functional language such as scala or ML; where programs are closer to mathematical models than in imperative languages)?
• Can bugs be avoided? Can the use of rigorous mathematical proofs guarantee that software and hardware perform as expected?
• Many projects and products dedicated to automated testing of program correctness, for example, VIPER or TestEra (automated testing of Java programs).
• What do proof obligations (Verpflichtung) have to do with the correctness of programs?: e.g. Barthe et al. discuss the “interaction between compilation and verification condition generators (VC generators), which are used in many interactive verification environments to guarantee the correctness of source programs, and by several proof carrying code (PCC) architectures to check the correctness of compiled programs. Such VC generators operate on annotated programs that carry loop invariants and procedure specifications expressed as preconditions and postconditions, and yield a set of proof obligations that must be discharged in order to establish the correctness of the program.” (loop and procedure level; see also specification languages such as CASL for the representation of precondition, invariants, and postconditions, i.e. proofs obligation)
• But correctness proof for a program, adds very little to one’s confidence in the program: “Beware of bugs in the above code: I have only proved it correct, not tried it. (Knuth)” (p.310)
• Checking new types of proofs: probabilistic, experimental, hybrid proofs (computation plus theoretical arguments) (p.311 ff.)

Further readings

• Hayashi (1998): Testing Proofs by Examples

Notes on (1) Cristian S. Calude et al. (2003) Passages of Proof and (2) Cristian S. Calude et al. (2004): Mathematical Proofs at a Crossroad .

Please note that the authors do not necessarily share my personal opinions and summaries on this page.

1. pre-Greek mathematics dominated by observation, intuition, experience
2. Greek deductive mathematics based on theorems; Euclid’s geometry; see also Pythagoras,Thales, Aristotle, Euclid, Archimedis. (Euclid became the reference for axiomatic-deductive thinking, see more recent works in mathematics, physics, computer science, biology, linguistics, which follow this tradition)
3. Mathematical language triggered by need for precision and rigour. Previously ordinary language was used “dominated by imprecision resulting from its predominantly spontaneous use, where emotional factors and lack of care have an impact”. Galilei, Descartes, Newton, Leibniz, … contribute to a shift from ordinary to a mixed language, i.e. ordinary language supplemented by an artificial component of symbols, formulas, and equations
4. The epsilon rigour; 19th century, Cauchy, Weierstrass (coping with processes with infinitely many steps such as limit, continuity, differentiability, and integrability)
5. The challenge of the principle of non–contradiction and the logical crisis (Russell–Whitehead, Hilbert, Brouwer); 19th/20th century; optimistic towards the possibility to arrange the whole mathematics as a formal system and to decide for any possible statement whether it is true or false.
6. Gödel’s incompleteness theorem (1931): “every formal system which is finitely specified, rich enough to include the arithmetic, and consistent (free of contradiction), is incomplete”, distinction between truth and provability (1:p.173 ff.); Chaitin (1975) suggests that complexity is a source of incompleteness
7. Reconciliation of empirical–experimental mathematics with deductive mathematics (today): Four-colour Problem (4CT; 1976; by Kenneth Appel & Wolfgang Haken; proof of 4CT by Neil Robertson, Daniel P. Sanders, Paul Seymour and Robin Thomas ; or the Kepler Conjecture by Thomas Hales) realized by the use of computer programs as pieces of mathematical proof
8. Quantization: Proofs are no longer exclusively based on logic and deduction, but also empirical and experimental.

• “A proof is a series of logical steps based on some axioms and deduction rules which reaches a desired conclusion. Every step in a proof can be checked for correctness by examining it to ensure that it is logically sound.” (1:p. 171)
• But who checks the proof (as human and Computer agents make mistakes)? Often proofs are falsified after having been published and then corrected (e.g. Appel/ Haken take on Kempe’s ideas). Some proofs cannot be checked by single humans (being to long and/or accomplished by computer-assistance) such as 4CT. (1:p. 171)
• “Mathematics cannot be conceived without proofs: [..] proofs and theorems go together; the object of a proof is to reach a theorem, while theorems are validated by proofs” (1:p.172).
• But: Mathematics is more than proofs. “What the mathematical community seems to value most are ideas. The most respected mathematicians are those with strong intuitions. (Harris)”. (1:p.172)
• Three dimensions of proofs:
  • syntactically: the formal proof, but “proof is only one step in the direction of confidence” (1:p.174, see Edmund Landau)
  • semantically: (truth value) “correctness by itself does not validate a proof, it is also necessary to understand it” (1:p.175; René Thom, Daniel Cohen, William Thurston) “the mission of mathematics is understanding”, consequently, computer-assisted proofs are harder to accept (see 4CT), but also deductive proofs are sometimes only understood by few mathematicians (see 1:p.176), “a theorem is validated if it has been accepted by a general agreement of the mathematical community” (Thom, 1:p.178), “a theorem is a statement that could be checked individually by a mathematician and confirmed also individually by at least two or three mathematicians, each of them working independently” (1:p.178) thus proposing the notion of an “agnogram … a theorem-like statement that we have verified as best we could, but whose truth is not know with the kind of assurance we attach to theorems and about which we must thus remain, to some extend, agnostic” (Swart, 1:p.178), “we believe the experts and we cannot tell for ourselves” (1:p.179), “mathematics occupies a special place [among other disciplines], where we believe anyone who claims to have proved a theorem on the say - so of just a few people - that is, until we hear otherwise” (1:p.179), “… in mathematics you can really argue that this is as close to absolute truth as you can get (Joe Spencer)” (1:p.179)
  • pragmatical: (relevance & use) “truth is not where you find it, but where you put it” (Perlis). “no matter how precise the rules are, we need human consciousness to apply the rules and to understand them and their consequences” (1:p.183)
• Aspects of mathematical proofs: deduction/ syllogistic reasoning (most visible aspect), but also: observation, intuition, experiment, visual representations, induction, analogy, and examples; some belonging to the preliminary steps, whose presence is not made explicit (when finally presenting the proof), but without which proofs cannot be conceived (2-p.17; see previous post); proving is a very heterogeneous process

• Proof by obviousness: “The proof is so clear that it need not be mentioned.”
• Proof by general agreement: “All in favour?”
• Proof by calculus: “This proof requires calculus, so we’ll skip it.”
• Proof by lost reference: “I know I saw it somewhere”
• Proof by necessity: “It had better be true, or the entire structure of mathematics would crumble to the ground.”
• Proof by plausibility: “It sounds good, so it must be true.”
• Proof by intimidation: “Don’t be stupid; of course it’s true.”
• Proof by terror: When intimidation fails
• Proof by lack of sufficient time: “Because of the time constraint, I’ll leave the proof to you.”
• Proof by tessellation: “This proof is the same as the last.”
• Proof by majority rule: Only to be used if general agreement is impossible
• Proof by authority: “Well, Don’t Knuth says it’s true, so it must be!”
• Proof by intuition: “I just have this gut feeling”

• equivalence between the logical and computational proofs
• logical/ conventional proofs: traditional; reasoning of humans (see Euclid, …); the logical process, i.e. finding a finite sequence of sentences strictly obeying some axioms and inference rules
• computational/ unconventional: computational process (machines are constructed based on sequences of sentences by humans) producing these sequences; but: proofs can contain steps that can never be verified by humans (based on the equivalence: development of artificial mathematicians, i.e. theorem provers such as Mathematica, Maple, MathLab)
• classical but unconventional proofs also comprise classical proof of excessive length and complexity (e.g. the classification of finite simple groups; 1:p.176/183)
• Artificial mathematicians are far less ingenious and subtle than human mathematicians, but they surpass their human counterparts by being infinitely more patient and diligent.
• Towards quantum computational proofs: conversion from computation into a sequence of sentences may not longer be possible, quantum automation are able to check a proof, but fail to reveal a “trace” of the proof (we don’t why it true), (quasi-empirical) quantum proofs might influence how we learn/ understand mathematics; leading to new ways to understand (and practice) mathematics, although we might not fully accept/trust unconventional proofs, the computational result is “a mathematical activity because it advances our knowledge of mathematics” (1:p.184)
• Overall: “There is little difference between traditional and unconventional types of proofs as [..] i) mathematical truth cannot always be certified by proof, ii) correctness is not absolute, but almost certain, as mathematics advance by making mistakes and correcting and re-correcting them (see Lakatos), iii) non-deterministic and probabilistic proofs do not allow mistakes in the applications of rules, the are just indirect forms of checking, iv) the explanatory component, the understanding emerging from proofs [..] is subjective and has no bearing on formal correctness.” (1:p.184)
• “Experimental Mathematics - as systematic mathematical experimentation ranging from hypotheses building to assisted proofs and automated proof-checking-will play an increasingly important role and will become part of the mainstream of mathematics. There are many reasons for this trend: They range from logical (the absolute truth simply doesn’t exist), sociological (correctness is not absolute [..]), economic (powerful computers will be accessible to more and more people), and psychological (results and success inspire emulation)” (2-p.26)

Knowledge is acquired through reason and by experiment: Should proofs belong exclusively to logic? Or should we also accept empirical-experimental arguments? Towards blending logical and empirical-experimental arguments. There is hope for integration! (see also next post)

I had a chat with Christian Hirsch today. In his PhD he has developed the semantic visual wiki Thinkbase, which combines the two commercial tools thinkmap and the semantic wiki freebase. Thinkbase is a visual wiki in that it provides an interactive graph using the semantic data of freebase. Users can use the graph to browse the wiki and may also access other web-content, such as Wikipedia. However, being based on two commercial tools, his implementation is not open-source. But he might be able to re-implement his code and provide it as open-source.

Thinkbase: Mapping the World's Brain

Based on his implementation for Thinkbase, he has developed Thinkfree, which is an application of thinkbase for the IT department of the University of Auckland and ProcessMapper, which visualizes a business process, i.e. the enrolment at the university (both internal tool, access via Intranet only). The latest prototype is Thinkpedia, a visualization of Wikipedia. It will be online soon.

For his PhD thesis he is aiming at developing a meta-tool that may be used to create a visual extension to semantic wikis and other web-based application. Moreover, he will look at other possible application for his graph-based navigation, such as personalized adaptation (filtering or recommendation) and more.

Further Reading

• coming up: Publication at HICSS
• Short paper at ISWC
• Google TechTalk by Christian’s supervisor John Gordon Hosking
• another visual wiki: Viki: A visual wiki design

I recently read a paper by Bent Flyvbjerg in which he discusses and justifies the usefulness of case study/ case methodology in social science. I am wondering whether and how is assumptions can be applied to mathematics. I am not summarizing the paper and am not providing its application to math; but simply sketch my thoughts.

Old-fashioned definition: “Case Study. The detailed examination of a single example of a class of phenomena, a case study cannot provide reliable information about the broader class, but it may be useful in the preliminary stages of an investigation since it provides hypotheses, which may be tested systematically with a larger number of cases. (Abercrombie, Hill, & Turner, 1984, p. 34)”

Cases in mathematics:

Claim: “General, theoretical (context-independent) knowledge is not more valuable than concrete, practical (context-dependent) knowledge”.

Bent Flyvbjerg discusses the role of cases and theory in human learning and emphasises that case study (e.g. carefully chosen experiments, experiences, cases) produces the type of (concrete, practical) context-dependent knowledge that research on learning shows to be necessary to allow people to develop from rule-based beginners to virtuoso experts. In contrast, textbooks provide (general, theoretical) context-independent theories (focus on universals) and bring the students just to a beginner’s level.

(This supports our work towards context-dependent mathematical learning objects; although we have so far defined context by the logical/ narrative/ social relation of mathematical knowledge — but maybe by”social” we actually mean concrete/ individualized/ practical aspects)

We make use of cases in mathematics (and maybe should adapt mathematical learning respectively rather than solely presenting abstract/ universal theories): William Farmer one’s told me about a colleague who had to give a lecture on algebra unprepared. Consequently, when presenting a proof, he had to continuously revise his steps, wipe the board, and start over again. This incremental approach actually helped the students to really understand how mathematics is practised, i.e. that the universal and abstract theories are not invented from scratch but have to be iteratively developed based on many cases — examples, counterexamples, etc. And also Cristian Calude has recently pointed out once more that the way of doing math cannot at all be compared to the way of presenting the final results!

Generalization and Force of Example

Claim: “One can often generalize on the basis of a single case (i.e. does not necessarily need statistics/ quantitative studies), and the case study may be central to scientific development via generalization as supplement or alternative to other methods. But formal generalization is overvalued as a source of scientific development, whereas the force of example is underestimated.”

In “Mathematical Naturalism” Philip Kitcher illustrates that the development of mathematics can be seen as a stepwise process from generalizations to their symbolic substitutes. Kitcher underlines the dynamics in mathematics, i.e. the creating, revising, and dismissing of mathematical knowledge, as well as the process of abstracting experiences to gain symbolic substitutes.

So what is the value of generalization and examples in mathematics? Although finding mathematical results is based on a case-based generalization process, mathematicians are particular interested in discussing the final general, abstract, and universal structures rather than looking at the concrete objects. However, particularly in teaching examples and exercises are essential, they help teachers to guide students from theory to theory (Michael Kohlhase says examples are theory morphism, i.e. “structure-preserving mappings between two mathematical structures.”).

Claim: “The case study is useful for both generating and testing of hypotheses but is not limited to these research activities alone.”

Bent Flyvbjerg cites Eckstein, John Walton, Karl Popper, who underline that case study is a mean for testing theories (Eckstein), produces the best theories (Walton), and is ideal for generalizing using falsification (critical reflexivity) (Popper). In the paper, theory is defined in two ways …

“[..] theory in its “hard” sense, that is, comprising explanation and prediction [..] theory in the “soft” sense, that is, testing propositions or hypotheses” [..]

See wikipedia definition of theory, mathematical theory and list of first-order theories. See also “A shorter model theory” by Wilfrid Hodges (1997).

“In mathematical logic, a theory is a set of sentences in a formal language. One way to specify a theory is to define a set of axioms. The theory can be taken to include just those axioms, or their logical or provable consequences, as desired.”

“A syntactically consistent theory is a theory from which not every sentence in the underlying language can be proved.”

“A satisfiable theory is a theory that has a model. This means there is a structure M that satisfies every sentence in the theory. “

Falsification is widely used to test and, if needed, refute mathematical theories: “If just one observation does not fit with the proposition, it is considered not valid generally and must therefore be either revised or rejected.” (cf. Flyvbjerg).

Claim: “The generalizability of case studies can be increased by the strategic selection of cases. When the objective is to achieve the greatest possible amount of information on a given problem or phenomenon, a representative case or a random sample may not be the most appropriate strategy. This is because the typical or average case is often not the richest in information. Atypical or extreme cases often reveal more information because they activate more actors and more basic mechanisms in the situation studied.”

This takes on the discussion by Kerber et. al., which have addressed the typicality of examples. However, in mathematics (in particular teaching) we also make us of atypical examples, counter examples, and near-miss examples. (Note, we might want to use our study of typical examples to eventually identify atypical examples. Moreover, we might want to apply the types of cases by Flyvbjerg to mathematical examples and exercises)

Flyvberg presents several strategies for selection different cases (see figure below): Among others …

• extreme cases: Getting a point across in an especially dramatic way, see e.g. Normen’s motivative example for management of change — Adriane 5
• critical cases: Require experience, looking for “most likely” and “least likely” cases, i.e. cases to either clearly confirm or irrefutably falsify propositions and hypothesis
• paradigmatic cases: Cases that highlight more general characteristics of the societies in questions; Kuhn showed that scientific paradigms cannot be expressed as rules and theories as there exists no predictive theories how predictive theory comes out; discovering paradigmatic cases requires intuition and taken-for-granted procedures

Strategies for the Selection of Samples and Cases

Do Case Studies Contain a Subjective Bias?

According to Flyvbjerg, it is falsification, not verification, that characterizes the case study. Moreover, the question of subjectivism and bias toward verification applies to all methods, not just to the case study.

This question also applies to mathematics. Rarely any human being is able to provide fully objective illustration, thus, also mathematical results have an individual touch and can include subjective, context-dependent parts influenced by the type of problem or personal views. In mathematics, single subjective cases do not lead to accepted and verified results. Instead we can observe a communal and peer-reviewed process within which a given proof is falsified and tested (see discussion with Cristian Calude).

Case studies often contain a substantial element of narrative. Good narratives typically approach the complexities and contradictions of real life. Accordingly, such narratives may be difficult or impossible to summarize into neat scientific formulae, general propositions, and theories.

I recommend to read pages 238-239, as Flyvberg’s illustration open a very new perspective on our work on mathematical examples (see below): “The opposite of summing up and “closing” a case study is to keep it open. [..] I tell the story in its diversity [..] I avoid linking the case with the theories [..] Instead, I relate the case to broader philosophical positions that cut across specializations. In this way, I try to leave scope for readers of different backgrounds to make different interpretations and draw diverse conclusions regarding the question of what the case is a case of. [..] Case study is a “virtual reality” [..] Students can safely be let loose in this kind of reality, which provides a useful training ground with insights into real-life practices that academic teaching often does not provide. [..]“ … maybe mathematical examples are more than theory morphisms (i.e. clear mappings between theories), maybe that have to leave room for imagination and interpretation. However, math is different to social science such as political studies or philosophy and mathematical knowledge is of a very different kind then social-science knowledge: it is abstract, well-structured, extraordinary interlinked, has a precise syntax and semantics. Well, but these characteristics make access to mathematical knowledge also so hard for novice: Maybe before being abstracted into clear structures in the human mind it has to be of a different form to be more easily understood by novice.

“One might say that the rule formulation that takes place when researchers summarize their work into theories is characteristic of the culture of research, of researchers, and of theoretical activity, but [..] something essential may be lost by this summarizing [..] “

This is indeed a problem in mathematics: When getting reading to write down their mathematical concepts, mathematicians do not fully articulate their thoughts but leave out parts that well-experienced mathematicians can fill in. However, students are lacking the observations/ experiences/ examples/ cases that experts have acquired through-out the years and have difficulties in understanding theoretic and abstract writings.

Further Reading

• Robert Stake’s (1995): The Art of Case Study Research
• Charles Ragin and Howard Becker’s (1992): What Is a Case?
• Scenario-based techniques

My first meeting with Cristian Calude has brought up many interesting aspects and thoughts, I shortly sketch here and I do not yet fully understand …
Please note that Cris and all other researchers mention do not necessarily share my personal opinions and summaries on this page.

• Mathematical Collaboration: In mathematics (and other disciplines), interdisciplinary authors often only know parts of the paper they co-author. If you contact one for the authors, your are sometimes directed to the original writer, as your contact might now able to tell you about all paragraphs in the paper. Cris has experienced this during papers with Chaitin, also both are well-experienced mathematicians, they have different ways of thinking (more visual in contrast to more analytical thinking), which sometimes made it difficult to understand each other’s solution.
• Mathematical Proofs: Cris’s friend, a logician, never looks at proofs. If he likes a theorem, he tries to proof it himself, but studying other people’s proof is not of interest for him
• Mathematical Practice: There is a research group of ethno-mathematicians here at the University of Auckland (e.g. see Bill Barton) looking at questions such as: How does the mother tongue language influence mathematics? Are the metaphors in different languages the same?
• Struggling with Notations: When giving a lecture in Leibzig, Chris experienced that the students struggled with his lecture. They understood the ideas, but when it came to solving assignments and applying the concepts in the lecture, they struggled with notations introduced by Chris as they had learned others.
• Mathematicians and Computers: Chris pointed to an interesting question: How can we train mathematicians to use computers and not to be afraid of their results (i.e. trust in automatic proofs)?. Many parts are implicit when proving, but computers need everything explicated. We have to ways of bringing mathematicians and computers closer together: (1) Making automatic provers more accessible and human-oriented, i.e. decreasing the level of formality needed for interacting with formal prove systems (see MKM proceedings on e.g. Mizar, i.e. “an attempt to reconstruct mathematical vernacular into a formal language which can be read by humans and also verified by software”, or Coq, Mathematica) and (2) Training mathematicians so that their encodings are more accessible for machines, i.e. in order to use computers, mathematicians need to change their way of encoding knowledge.
• Mathematicians and Computers: For (2), Chris suggested to start at looking at referee processes: What kind of questions does a referee ask? What aspects do mathematical referee look at? They mostly do not fully check the presented proof and pose specific questions which may help us to identify how knowledge has to be encoded to be communicated more efficiently (between humans and eventually between humans and computers).
• Mathematical Practice: There are two processes in mathematics: (1) The process of discovery, which is very informal, includes several gaps, and is a slow and iterative approaching of a more and more coherent solution. (2) The process of presenting a result, i.e. the writing up of a solution. Both processes are valuable. We know several tools supporting (2) and in our group we also aim at supporting this process (with a Wiki for collaborative editing and a management of change system, …). However, process (1) requires tools that do not kill the creativity of mathematicians, i.e. that do not enforce notations/ styles and require tedious and correct mark-up of thoughts … but leave room for intuitions, gaps, and mistakes. And also eLearning systems (e.g. panta-rhei) should support process (1) as mathematical education should not focus on the presentation of results but should teach students how to discover math. However, towards the end of process (1), mathematicians might have to/ want to draw on computers (theorem provers and computer algebra systems) to verify their results.
• Confidence in and Acceptance of proofs: In mathematics we observe different degrees of confidence of a proof, i.e. a proof is accepted in a social process and on different layers: (1) It can be published in a journal (and thus reviewed and accepted by the journal chairs) and (2) it can be accepted by reviewers of the two reviewing databases, Mathematical Reviews and Zentralblatt, and (3) it can be certified (i.e. verified by computers; see e.g. Coquand et al). Moreover, (4) the credibility of a theory increases with the number of proofs for its theorems (see e.g. collection of 79 approaches to proving the Pythagorean theorem) and its use in different context (I am not yet sure what Cris means by context. My first guess is that this relates to the reuse of a theory and its interrelation to other theories, i.e. the number of views and theory morphism. Basically, the structures that were used by Immanuel and Florian to do their PhD on logic translation and theory management; see next meeting). To sum up, a proof is not necessarily correct, but its confidence can increase.
• Communal Acceptance: The Clay Mathematics Institute of Cambridge, Massachusetts (CMI) nominates its Millennium Prize Problems for one million dollar. The respective proof has to be published and resist community testing for 2 years. Thus, the mathematical community is very aware of the fact that only publishing a proof does not mean that it is correct.

Further readings

• Cristian S. Calude etAl (2003): Passages of Proof (see my notes; slides)
• Cristian S. Calude etAl (2004): Mathematical Proofs at a Crossroad? (see my notes)
• Cristian S. Calude etAl (2007): Proving and Programming (slides)
• Calude/ Chaitin (2006) A Dialogue on Mathematics & Physics
• see Platonic universe of mathematical ideas
• Ethnomathematics and its First International Congress (the why’s and when of etchnomathematics)
• Bill Barton (1996): Ethnomathematics: Exploring Cultural Diversity in Mathematics (also recommended by Patrick Johnson)
• 2000 Mathematics Subject Classification (pdf)
• “Formalizing mathematical proofs has as aim to represent arbitrary mathematical notions and proofs on a computer in order to construct a database of certified results useful to learn and develop the subject [..]” such as the proof-assistant Mizar, Coq, etc. (cf. Barendregt)
• Coquand et al (2003): [..] a certificate … represents the information needed to complete a proof of correctness of the mathematical data.
• newscientist.com (2006) Mathematical proofs getting harder to verify: “A mathematical proof is irrefutably true, a manifestation of pure logic. But an increasing number of mathematical proofs are now impossible to verify with absolute certainty, according to experts in the field.”

(copied from the call for participation)

Alan Lightman is a novelist, essayist, physicist, and educator. Currently, he is Adjunct Professor of Humanities at the Massachusetts Institute of Technology (MIT).

The Discoveries
Several years ago, Alan Lightman asked physicists, chemists and biologists to nominate the most important scientific discoveries in the twentieth century in their respective fields. He condensed this list to about two dozen discoveries, which included the discovery of the first hormone, the discovery of special relativity, the discovery of the uncertainty principle, the discovery how nerves communicate with each other, the discovery of the structure of DNA, the discovery of the chemical bond.

In this lecture, drawing on his book The Discoveries, Professor Lightman will review some of these landmark scientific discoveries and briefly describe the impact and significance of the work, as well as talk about the personalities and human drama of the scientists involved and some common patterns in the process of discovery.

Flexible, autonome Verhaltenskontrolle: Erlernen und Adaptation von Sensormotorischen Raumrepräsentationen
Keynote by Martin Butz (COBOSLAB, University of Würzburg) at Lernen, Wissen, Adaptivität (LWA 2008), University of Würzburg, 6.-8. October 2008. Track: FGWM

Evaluating Tools of the X-COSIM Semantic Desktop
Presentation by Thomas Franz at Lernen, Wissen, Adaptivität (LWA 2008), University of Würzburg, 6.-8. October 2008. Track: FGWM

Hypothesis: PIM benefits from information linkage and information reuse across PIM application.
Method: Using RDF and Semantic Web technologies.

X-COSIM provides the X-COSIMO ontology:
Among others, X-COSIMO defines contextual information in a formal representation for context, the contextual ontology includes concepts such as email, attachment, sender, recipients. Attachments e.g. contextualizes information object, while sender and recipient contextualizes agents in the systems.

Evaluation:
Does an X-COSIM enabled desktop provide better support for PIM tasks than a conventional one?
Better means: increased effectiveness (absolute time spend on each task), increased efficiency (goals reached: distance of mouse movements, number of window switches, …), increased satisfaction (questionnaire, ratings, interview).

• 18 participants: 3 graduate students and 15 Ph.D.s students; none of them used the semantic desktop before.
• Introduction (to the scenario, to the dataset, get acquainted to the system), observation, and feedback phase.
• Scenario: Real data select from the organizers of the Night of Computer Science in Koblenz (more than 140 emails, 44 files, 40 files via eMail, …)
• Tasks: (1) organization tasks (familiarization: all emails in one folder and participants had to create a folder structure), (2) lookup tasks (baseline: re-finding information; baseline as this feature was not expected to be of greater benefit in contrast to others), (3) multi-item tasks (evaluation), (4) document-driven collaboration (evaluation), (5) information collation (evaluation)
• Evaluation Wizard: guiding the user through the evaluation; presenting the lookup tasks, …, and questionnaire. The wizard tracked the execution time for each task.

Results: Semantic desktop can improve PIM.

Implementation: Runs on KDE with Thunderbird. download now