Catálogo de publicaciones - libros

We describe a case-study of the application of web- technology (Helm 2) to create web-based didactic material out of a repository of formal mathematics (C-CoRN 5), using the structure of an existing course (IDA 4). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the “view”), and the rendering of proofs.

A variety of problems in mathematical calculus can be solved by recursively applying a finite number of rules. Often, a generic solving strategy can be extracted and an interactive exercise system that emulates a tutor can be implemented.

In this paper we show how software developed by us can be used to realize this interactivity. In particular, an implementation of a generic exercise for computing the derivative of elementary functions is presented.

Since version 7.2 the Mizar system produces quite detailed XML-based semantic description of Mizar articles during their verification. This format is now used natively for most of the processing done by Mizar, e.g., also for the whole Mizar internal database. The main motivation for switching to this XML-based representation is to make semantic communication with Mizar and presentation of the MML more accessible to a variety of external tools and systems. This article briefly describes this format and its current implementation, and shows examples of its usage. These examples include presentation of linked Mizar articles in modern XML-capable browsers like Mozilla, authoring assistance in the Mizar mode for Emacs, and experiments with XML-based querying languages like XQuery over the Mizar Mathematical Library loaded into a native XML databases like eXist. This work makes the currently largest repository of formal mathematics available to many kinds of presentational, data-mining, and automated reasoning applications and experiments, and the goal of this article is also to encourage, facilitate and provide recipes for the development of such applications.

Many processes in mathematical computing try to use knowledge of the most desired forms of mathematical expressions. This occurs, for example, in symbolic computation systems, when expressions are simplified, or mathematical document recognition, when formula layout is analyzed. The decision about which forms are the most desired, however, has typically been left to the guess-work or prejudices of a small number of system designers.

This paper observes that, on a domain by domain basis, certain expressions are actually used much more frequently than others. On the hypothesis that actual usage is the best measure of desirability, this papers begins to quantify empirically the use of common expressions in the mathematical literature. We analyze all 20,000 mathematical documents from the mathematical arXiv server from 2000-2004, the period corresponding to the new mathematical subject classification. We report on the process by which these documents are analyzed, through conversion to MathML, and present first empirical results on the most common aspects of mathematical expressions by subject classification. We use the notion of a weighted dictionary to record the relative frequency of subexpressions, and explore how this information may be used for further processes, including deriving common patterns of expressions and probability measures for symbol sequences.

The main goal of most systems for formalizing mathematics is creating the database of formalized knowledge. Every system uses its own way of storing that knowledge. Pieces of the information stored in such a database are something more than just elements of that database – we may also look at it from another perspective. Namely, the information is the reflection of some text and that text is the representation of some logical reasoning. Therefore every such piece of information may be treated as an element of some set and then we may analyze the relationships between all these elements. This article describes such an approach to one of the systems for formalizing mathematics.

One of the main application areas of interactive proof assistants is the formalization of mathematical texts. This formalization not only allows mathematical texts to be handled electronically, but also to be checked for correctness. Due to the level of detail required in the formalization, formalized texts eliminate ambiguities that may be present in an informally presented mathematical texts.