Catálogo de publicaciones - libros

Literate proving is the analogue for literate programming in the mathematical realm. That is, the goal of literate proving is for humans to produce clear expositions of formal mathematics that could even be enjoyable for people to read whilst remaining faithful representations of the actual proofs. This paper describes maze, a generic literate proving system. Authors markup formal proof files, such as Mizar files, with arbitary XML and use maze to obtain the selected extracts and transform them for presentation, e.g. as LATEX. To aid its use, maze has built in transformations that include pretty printing and proof sketching for inclusion in LATEX documents. These transformations challenge the concept of faithfulness in literate proving but it is argued that this should be a distinguishing feature of literate proving from literate programming.

The amount of machine oriented data on the web as well as the deployment of agent/Web Services are simultaneously increasing. This poses a service-discovery problem for client agents wishing to discover Web Services to perform tasks. We discuss a prototype mathematical service broker and look at an approach to circumventing the ambiguities arising from alternative but equivalent mathematical representations occurring in mathematical descriptions of tasks and capabilities.

Mathematical OCR (Optical Character Recognition) systems retrieve character sequences and the structure of mathematical formulae from raster images scanned from mathematical documents. In this paper a method for detecting hyperlinks, e.g. formula links, from mathematical OCR output is described. We also experimentally demonstrated the effectiveness of the method. By using the method we implemented a prototype system of a mathematical knowledge browser that helps people read mathematical articles.

Automatic document analysis tools for mathematical texts are necessary to enlarge the pool of mathematical knowledge available in electronic form. However, development of such tools is currently hindered by the weakness of optical character recognition systems in dealing with the large range of mathematical symbols and the often subtle but important distinctions in font usage in mathematical texts. Research on developing better systems for mathematical optical character recognition crucially depends on having an extensive, high quality database of glyphs used in mathematical texts for training and test purposes. We present such a database of symbols constructed from a large set of characters available in the LATEX document preparation system that can serve as a basis mathematical text recognition. We describe its integration into a prototypical system optical character recognition system for mathematics that enables the construction of LATEX source documents from mathematical documents available as images. From the lessons learned in this work we derive a road map for further research into the area of mathematical text analysis.

Computerizing mathematical texts to allow software access to some or all of the texts’ semantic content is a long and tedious process that currently requires much expertise. We believe it is useful to support computerization that adds some structural and semantic information, but does not require jumping directly from the word-processing level (e.g., LATEX) to full formalization (e.g., Mizar, Coq, etc.). Although some existing mathematical languages are aimed at this middle ground (e.g., MathML, OpenMath, OMDoc), we believe they miss features needed to capture some important aspects of mathematical texts, especially the portion written with natural language. For this reason, we have been developing MathLang, a language for representing mathematical texts that has weak type checking and support for the special mathematical use of natural language. MathLang is currently aimed at only capturing the essential grammatical and binding structure of mathematical text without requiring full formalization.

The development of MathLang is directly driven by experience encoding real mathematical texts. Based on this experience, this paper presents the changes that yield our latest version of MathLang. We have restructured and simplified the core of the language, replaced our old notion of “context” by a new system of blocks and local scoping, and made other changes. Furthermore, we have enhanced our support for the mathematical use of and with object-oriented features so that nouns now correspond to , and adjectives to .

The λ̄μμ͂-calculus, introduced by Curien and Herbelin, is a calculus isomorphic to (a variant of) the classical sequent calculus LK of Gentzen. As a proof format it has very remarkable properties that we plan to study in future works. In this paper we embed it with a rendering semantics that provides explanations in pseudo-natural language of its proof terms, in the spirit of the work of Yann Coscoy [3] for the -calculus. The rendering semantics unveils the richness of the calculus that allows to preserve several proof structures that are identified when encoded in the -calculus.

Due to their rapidly increasing amount, maintaining mathematical documents more and more becomes an engineering task. In this paper, we combine the projects MMISS and CDET. That way, we achieve major benefits for mathematical knowledge management: (1) Semantic annotations relate mathematical constructs. This reaches beyond mathematics and thus fosters integration of mathematical content into a broader context. (2) Fine-grained version control enables change management and configuration management. (3) Semi-formal consistency management identifies violations of user-defined consistency requirements and proposes how they can be best resolved.

We present a computational origami construction of Morley’s triangles and automated proof of correctness of the generalized Morley’s theorem in a streamlined process of solving-computing-proving. The whole process is realized by a computational origami system being developed by us. During the computational origami construction, geometric constraints in symbolic and numeric representation are generated and accumulated. Those constraints are then transformed into algebraic relations, which in turn are used to prove the correctness of the construction. The automated proof required non-trivial amount of computer resources, and shows the necessity of networked services of mathematical software. This example is considered to be a case study for innovative mathematical knowledge management.

The use of diagrammatic representations as is analyzed using an example of the catalogue of types of the basic interval equation · =. The procedure of finding and describing the types is outlined and a number of different diagrammatic and tabular catalogues are presented and their drawbacks and merits discussed. Suggestions for other solutions, like different forms of the catalogue and interactive catalogue are included. Some preliminary guidelines for designing such catalogues are formulated as well.

We argue that for building mathematical knowledge repositories a broad development of theories is of major importance. Organizing mathematical knowledge in theories is an obvious approach to cope with the immense number of topics, definitions, theorems, and proofs in a general repository that is not restricted to a special field. However, concrete mathematical objects are often reinterpreted as special instances of a general theory, in this way reusing and refining existing developments. We believe that in order to become widely accepted mathematical knowledge management systems have to adopt this flexibility and to provide collections of well-developed theories.

As an example we describe the Mizar development of the theory of Gröbner bases, a theory which is built upon the theory of polynomials, ring (ideal) theory, and the theory of rewriting systems. Here, polynomials are considered both as ring elements and elements of rewriting systems. Both theories (and polynomials) already have been formalized in Mizar and are therefore refined and reused. Our work also includes a number of theorems that, to our knowledge, have been proved mechanically for the first time.