Conferences on Intelligent Computer Mathematics 2010

The 9th International Conference on
Mathematical Knowledge Management

MKM 2010

Paris, France    8th-9th July 2010


Conference Programme    

Thursday, July 8th 2010

Welcome (13:50-14:00)

Invited Talk (14:00-15:00, Chair: Patrick Ion)

14:00-15:00 Can we make Mathematics universal as well as fully reliable?
Pierre Cartier

Abstract: These are times of change for the mathematical profession and for the practice of mathematics, with, for instance, the advent of powerful computing machinery and the extraordinary immediacy of communication all over the world. If the concept of globalization has any meaning, this is now the time of globalization in mathematics. The pretense of mathematics of being universal can now be made real, and mathematical knowledge be shared by people from many different backgrounds. In addition, there is now mechanical help in reasoning, digitization of large parts of the traditional mathematical literature, and amazing amounts of scientific data and problems begging analysis which all help to offer a change in the role of mathematics. Checking proofs by computers is just one of the many new possibilities. A new paradigm is needed to understand a world of TERABYTES, where the frontier between "proof" and "guess" is quite fuzzy. Between "finite" and "infinite", we have to introduce in our axiomatics the world of "very very large".

Break (15:00-15:30)

Session 1 (15:30-16:30, Chair: Bruce Miller)

15:30-16:00 Towards MKM in the Large: Modular Representation and Scalable Software Architecture
Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev

Abstract: MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM “in the small” is well-studied, so the real problem is to scale up to large, highly interconnected corpora: “MKM in the large”. We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases.
We present instances of both in this paper: the MMT framework for modular theory-graphs that integrates meta-logical foundations, which forms the base of the next OMDOC version; and TNTBase, a versioned storage system for XMLbased document formats. TNTBase becomes an MMT database by instantiating it with special MKM operations for MMT.

[Preprint]     [Springerlink]
16:00-16:30 Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System
Xiaoyu Chen

Abstract: Electronic Geometry Textbook is a knowledge management system that manages geometric textbook knowledge to enable users to construct and share dynamic geometry textbooks interactively and efficiently. Based on a knowledge base organizing and storing the knowledge represented in specific languages, the system implements interfaces for maintaining the data representing that knowledge as well as relations among those data, for automatically generating readable documents for viewing or printing, and for automatically discovering the relations among knowledge data. An interface has been developed for users to create geometry textbooks with automatic checking, in real time, of the consistency of the structure of each resulting textbook. By integrating an external geometric theorem prover and an external dynamic geometry software package, the system offers the facilities for automatically proving theorems and generating dynamic figures in the created textbooks. This paper provides a comprehensive account of the current version of Electronic Geometry Textbook.

[Preprint]     [Springerlink]

Coffee Break (16:30-17:00)

Session 2 (17:00-18:30, Chair: Stephen Watt)

17:00-17:30 The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents
Andriy Kovalchuk, Vyacheslav Levitsky, Igor Samolyuk, Valentyn Yanchuk

Abstract: Implementation of an editing process for Content MathML formulas in common visual style is a real challenge for a software developer who does not really want the user to have to understand the structure of Content MathML in order to edit an expression, since it is expected that users are often not that technically minded. In this paper, we demonstrate how this aim is achieved in the context of the Formulator project and discuss features of this MathML editor, which provides a user with a WYSIWYG editing style while authoring MathML documents with Content or mixed markup. We also present the approach taken to enhance availability of the MathML editor to end-users, demonstrating an online version of the editor that runs inside a Web browser.

[Preprint]     [Springerlink]
17:30-18:00 A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers

Abstract: Formal mathematics has so far not taken full advantage of ideas from collaborative tools such as wikis and distributed version control systems (DVCS). We argue that the field could profit from such tools, serving both newcomers and experts alike. We describe a preliminary system for such collaborative development based on the Git DVCS. We focus, initially, on the Mizar system and its library of formalized mathematics.

[Preprint]     [Springerlink]
18:00-18:30 Proofs, proofs, proofs, and proofs
Manfred Kerber

Abstract: In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence. Sociologically, however, it is more difficult to say what should constitute a proof and what not. In this paper we will look at different forms of proofs and try to clarify the concept of proof in the wider meaning of the term. This has implications on how proofs should be represented formally.

[Preprint]     [Springerlink]

Friday, July 9th 2010

Session 3 (09:00-10:30, Chair: Michael Kohlhase)

09:00-09:30 Evidence Algorithm and System for Automated Deduction: A Retrospective View
Alexander Lyaletski, Konstantin Verchinine

Abstract: A research project aimed at the development of an automated theorem proving system was started in Kiev (Ukraine) in early 1960s. The mastermind of the project, Academician V.Glushkov, baptized it “Evidence Algorithm“, EA. The work on the project lasted, off and on, more than 40 years. In the framework of the project, the Russian and English versions of the System for Automated Deduction, SAD, were constructed. They may be already seen as powerful theorem proving assistants. The paper gives a retrospective view to the whole history of the development of the EA and SAD. Theoretical and practical results obtained on the long way are systematized. No comparison with similar projects is made.

[Preprint]     [Springerlink]
09:30-10:00 On Building a Knowledge Base for Stability Theory
Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller

Abstract: A lot of mathematical knowledge has been formalized and stored in repositories by now: Different mathematical theorems and theories have been taken into consideration and included in mathematical repositories. Applications more distant from pure mathematics, however — though based on these theories — often need more detailed knowledge about the underlying theories. In this paper we present an example Mizar formalization from the area of electrical engineering focusing on stability theory which is based on complex analysis. We discuss what kind of special knowledge is necessary and which amount of this knowledge is included in existing repositories.

[Preprint]     [Springerlink]
10:00-10:30 On Duplication in Mathematical Repositories
Adam Grabowski, Christoph Schwarzweller

Abstract: Building a repository of proof-checked mathematical knowledge is without any doubt a lot of work, and besides the actual formalization process there is also the task of maintaining the repository. Thus it seems obvious to keep a repository as small as possible, in particular each piece of mathematical knowledge should be formalized only once. In this paper, however, we claim that it might be reasonable or even necessary to duplicate knowledge in a mathematical repository. We analyze different situations and reasons for doing so, provide a number of examples supporting our thesis and discuss some implications for building mathematical repositories.

[Preprint]     [Springerlink]

Coffee Break (10:30-11:00)

Session 4 (11:00-12:30, Chair: Volker Sorge)

11:00-11:30 An OpenMath Content Dictionary for Tensor Concepts
Joseph Collins

Abstract: We introduce a new OpenMath content dictionary named “tensor1” containing symbols for the expression of tensor formulas. These symbols support the expression of non-Cartesian coordinates and invariant, multilinear expressions in the context of coordinate transformations. While current OpenMath symbols support the expression of linear algebra formulas using matrices and vectors, we find that there is an underlying assumption of Cartesian, or standard, coordinates that makes the expression of general tensor formulas difficult, if not impossible. In introducing these new OpenMath symbols for the expression of tensor formulas, we attempt to maintain, as much as possible, consistency with prior OpenMath symbol definitions for linear algebra.

[Preprint]     [Springerlink]
11:30-12:00 Smart matching
Andrea Asperti, Enrico Tassi

Abstract: One of the most annoying aspects in the formalization of mathematics is the need of transforming notions to match a given, existing result. This kind of transformations, often based on a conspicuous background knowledge in the given scientific domain (mostly expressed in the form of equalities or isomorphisms), are usually implicit in the mathematical discourse, and it would be highly desirable to obtain a similar behaviour in interactive provers. The paper describes the superposition-based implementation of this feature inside the Matita interactive theorem prover, focusing in particular on the so called smart application tactic, supporting smart matching between a goal and a given result.

[Preprint]     [Springerlink]
12:00-12:30 Proviola: a Tool for Proof Re-animation
Carst Tankink, James McKinna, Herman Geuvers, Freek Wiedijk

Abstract: To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we introduce three related concepts, those of: a proof movie, consisting of frames which record both user input and the corresponding PA response; a camera, which films a user’s interactive session with a PA as a movie; and a proviola, which replays a movie frame-by-frame to a third party. In this paper we describe the movie data structure and we discuss a prototype implementation of the camera and proviola based on the ProofWeb system. ProofWeb uncouples the interaction with a PA via a webinterface (the client) from the actual PA that resides on the server. Our camera films a movie by “listening” to the ProofWeb communication.
The first reason for developing movies is to uncouple the reviewing of a formal proof from the PA used to develop it: the movie concept enables users to discuss small code fragments without the need to install the PA or to load a whole library into it.
Other advantages include the possibility to develop a separate commentary track to discuss or explain the PA interaction. We assert that a combined camera+proviola provides a generic layer between a client (user) and a server (PA). Finally we claim that movies are the right type of data to be stored in an encyclopedia of formalized mathematics, based on our experience in filming the Coq standard library.

[Preprint]     [Springerlink]

Lunch (12:30-14:00)

Invited Talk (14:00-15:00, Chair: Alan Sexton)

14:00-15:00 Against Rigor
Doron Zeilberger

Abstract:The ancient Greeks gave (western) civilization quite a few gifts, but we should beware of Greeks bearing gifts. The gifts of theatre and democracy were definitely good ones, and perhaps even the gift of philosophy, but the "gift" of the so-called "axiomatic method" and the notion of "rigorous" proof did much more harm than good. If we want to maximize Mathematical Knowledge, and its Management, we have to return to Euclid this dubious gift, and give-up our fanatical insistence on perfect rigor. Of course, we should not go to the other extreme, of demanding that everything should be non-rigorous. We should encourage diversity of proof-styles and rigor levels, and remember that nothing is absolutely sure in this world, and there does not exist an absolutely rigorous proof, nor absolute certainty, and "truth" has many shades and levels.

Break (15:00-15:20)

Session 5 (15:20-16:30, Chair: Andrea Asperti)

15:20-15:40 Towards Automatic Formalization of Informal Mathematics with MathNat (presentation only)
Muhammad Humayoun and Christophe Raffalli

Abstract:Can we build a program that understands informal mathematical text and can we mechanically verify it's correctness? MathNat project aims at being a first step towards answering this question.
We develop a controlled language for mathematics (CLM), which is a precisely defined subset of English with restricted grammar and dictionary. Like textbook mathematics, CLM supports some complex linguistic features to make it natural and expressive.
For formalisation, we automatically translate CLM into a system-independent formal language (MathAbs). MathAbs can represent most of informal mathematical text. It also preserves the logical structure, proof steps and line of reasoning of a given math text. For verification, which is the second part of the question, we have done very limited work so far. Therefore we answer it partially and it needs to be explored further.
In this paper, we mainly focus on formalisation by giving a formal definition of MathAbs and by describing the algorithm which supports proof-by-case method in CLM. Further, we validate our work with two examples.

15:40-16:00 Integrating multiple sources to answer questions in Algebraic Topology (short paper)
Jönathan Heras, Vico Pascual, Ana Romero, Julio Rubio

Abstract: We present in this paper an evolution of a tool from a user interface for a concrete Computer Algebra system for Algebraic Topology (the Kenzo system), to a front-end allowing the interoperability among different sources for computation and deduction. The architecture allows the system not only to interface several systems, but also to make them cooperate in shared calculations.

[Preprint]     [Springerlink]
16:00-16:30 Dimensions of Formality: A Case Study for MKM in Software Engineering
Andrea Kohlhase, Michael Kohlhase, Christoph Lange

Abstract: We study the formalization of a collection of documents created for a Software Engineering project from an MKM perspective. We analyze how document and collection markup formats can cope with an open-ended, multi-dimensional space of primary and secondary classifications and relationships.We show that RDFa-based extensions of MKM formats, employing flexible “metadata” relationships referencing specific vocabularies for distinct dimensions, are well-suited to encode this and to put it into service. This formalized knowledge can be used for enriching interactive document browsing, for enabling multi-dimensional metadata queries over documents and collections, and for exporting Linked Data to the Semantic Web and thus enabling further reuse.

[Preprint]     [Springerlink]

Coffee Break (16:30-17:00)

Session 6 (17:00-18:30, Chair: William Farmer)

17:00-17:30 Adapting Mathematical Domain Reasoners
Bastiaan Heeren, Johan Jeuring

Abstract: Mathematical learning environments help students in mastering mathematical knowledge. Mature environments typically offer thousands of interactive exercises. Providing feedback to students solving interactive exercises requires domain reasoners for doing the exercise-specific calculations. Since a domain reasoner has to solve an exercise in the same way a student should solve it, the structure of domain reasoners should follow the layered structure of the mathematical domains. Furthermore, learners, teachers, and environment builders have different requirements for adapting domain reasoners, such as providing more details, disallowing or enforcing certain solutions, and combining multiple mathematical domains in a new domain. In previous work we have shown how domain reasoners for solving interactive exercises can be expressed in terms of rewrite strategies, rewrite rules, and views. This paper shows how users can adapt and configure such domain reasoners to their own needs. This is achieved by enabling users to explicitly communicate the components that are used for solving an exercise.

[Preprint]     [Springerlink]
17:30-18:00 sTeXIDE: An Integrated Development Environment for sTeX Collections
Constantin Jucovschi, Michael Kohlhase

Abstract: Authoring documents in MKM formats like OMDoc is a very tedious task. After years of working on a semantically annotated corpus of STEX documents (GenCS), we identified a set of common, time-consuming subtasks, which can be supported in an integrated authoring environment.
We have adapted the modular Eclipse IDE into STEXIDE, an authoring solution for enhancing productivity in contributing to STEX based corpora. STEXIDE supports context-aware command completion, module management, semantic macro retrieval, and theory graph navigation.

[Preprint]     [Springerlink]
18:00-18:30 Notations Around the World: Census and Exploitation
Paul Libbrecht

Abstract: Mathematical notations around the world are diverse. Not as much as requiring computing machines' makers to adapt to each culture, but as much as to disorient a person landing on a web-page with a text in mathematics.
In order to understand better this diversity, we are building a census of notations: it should allow any content creator or mathematician to grasp which mathematical notation is used in which language and culture. The census is built collaboratively, collected in pages with a given semantic and presenting observations of the widespread notations being used in existing materials by a graphical extract. We contend that our approach should dissipate the fallacies found here and there about the notations in “other cultures” so that a better understanding of the cultures can be realized.
The exploitation of the census in the math-bridge project is also presented: this project aims at taking learners “where they are in their math-knowledge” and bring them to a level ready to start engineering studies. The census serves as definitive reference for the transformation elements that generate the rendering of formulae in web-browsers.

[Preprint]     [Springerlink]

Closing Remarks (18:30-18:40)

MKM Business Meeting (18:40-19:30)