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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.