Catálogo de publicaciones - libros

The development of e-Science (cyberScience, Grid, etc.) is starting to become a reality with formalised data resources, services on demand, domain-specific search engines, digital repositories, etc. Increasingly STM information will be contained in compound XML documents, representing scientific communication (articles, theses, repository entries, etc.). In physical sciences such as chemistry, materials science, engineering, physics, earth sciences, these “datuments” [1] normally contain hypertext, graphics, tables, graphs and numerical data, mathematical objects and relationships. In addition they may also contain domain-specific content such as chemical formula and reactions, thermodynamic and mechanical properties, electric, magnetic and optical properties.

Among the domain-specific languages, CML (Chemical Markup Language) is the oldest and broadest, and is now being actively used for publishing by the Royal Society of Chemistry (Project Prospect [2]) which gives an idea of what chemistry in datuments can look like. CML has had to develop the domain-specific objects (molecules, atoms, bonds, spectra, crystallography, etc.) and the relationships between them. However, due to the text-based nature of early XML, it has also had to design an implement domain-independent infrastructure which can support much of physical science. Originally called STMML [3] it supports data types (float, integer, complex, etc.), data structures (arrays, lists, matrices, etc.), geometrical concepts (points, planes, lines, etc.) and scientific units of measurement. In addition CML bases much of its flexibility one usercreated dictionaries (ontologies) which are hyperlinked from objects in the datuments.

The On-Line Encyclopedia of Integer Sequences (or OEIS) is a database of some 130000 number sequences. It is freely available on the Web (http://www.research.att.com/~njas/sequences/) and is widely used.

There are several ways in which it benefits research:

The 40-year history of the OEIS recapitulates the story of modern computing, from punched cards to the internet.

The talk will be illustrated with numerous examples, emphasizing new sequences that have arrived in the past few months. Many open problems will be mentioned.

Because of the profusion of books and journals, volunteers play an important role in maintaining the database. If you come across an interesting number sequence in a book, journal or web site, please send it and the reference to the OEIS. (You do not need to be the author of the sequence to do this.) There is a web site for sending in ”Comments” or ”New sequences”.

Several new features have been added to the OEIS in the past year. Thanks to the work of Russ Cox, searches are now performed at high speed, and thanks to the work of Debby Swayne, there is a button which displays plots of each sequence. Finally, a ”listen” button enables one to hear the sequence played on a musical instrument (try Recamáan’s sequence A005132!).

A prototype for a web application designed to symbolically process locus, proof and discovery tasks on geometric diagrams created with the commercial dynamic geometry systems , and is presented. The application, named LAD (acronym for ) and thought of as a remote for the considered DGS, follows the Groebner basis method relying on CoCoA and a Mathematica kernel for the involved symbolic computations. From the DGS internal textual representation of a geometric diagram, an OpenMath (i.e. semantic based) description of the requested task is created using the elements in the OpenMath . A review of the elements included in these CDs is given and two new elements proposed, namely and . Everything is finally thoroughly illustrated with examples. LAD is freely accessible at .

In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a first order automatic proof searching procedure, in a restricted equational framework. The automatic procedure is based on superposition rules for the unit equality case. Proof transformation techniques aimed to improve the readability of the final proof are discussed.

This paper introduces , a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called . The main channel connects to . Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a middleware component which manages proof-in-progress and mediates between components.

In order to foster the use of proof assistance systems, we integrated the proof assistance system Ωmega with the standard scientific text-editor . We aim at a document-centric approach to formalizing and verifying mathematics and software. Assisted by the proof assistance system, the author writes her document entirely inside the text-editor in a language she is used to, that is a mixture of natural language and formulas in  style. We present a basic mechanism that allows the author to define her own notation inside a document in a natural way, and use it to parse the formulas written by the author as well as to render the formulas generated by the proof assistance system. To make this mechanism effectively usable in an interactive and dynamic authoring environment, we extend it to efficiently accommodate modifications of notations, to track dependencies to ensure the right order of notations and formulas, to use the hierarchical structure of theories to prevent ambiguities, and to reuse concepts together with their notation from other documents.

From the very beginning of the development of the system experiments with using as a tool for teaching mathematics have been conducted. Numerous organized courses were based on different versions of the system: starting from the first implementation of its processor, through , –4 and up till its present version. Now with its mathematical library gives us quite new didactic possibilities.

The purpose of this paper is to present a certain course on logic and set theory offered by our Institute for freshman students. The course employs as the main tool of instruction. In the paper we discuss the organization of this course and describe some examples of students’ tasks. Finally, some conclusions and remarks are given.

Formal concept analysis (FCA) comprises a set of powerful algorithms which can be used for data analysis and manipulation, and a set of visualisation tools which enable the discovery of meaningful relationships between attributes of the data. We explore the potential of combining FCA and mathematical discovery tools in order to better facilitate discovery tasks. In particular, we propose a novel lookup method for the Encyclopedia of Integer Sequences, and we show how conjectures from the Graffiti discovery program can be better understood using FCA visualisation tools. We argue that, not only can FCA tools greatly enhance the management and visualisation of mathematical knowledge, but they can also be used to drive exploratory processes.

We present a new framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable version of their work. We describe a prototype based on Coq, its web interface as implemented by the second author, and a modified version of the MediaWiki code-base. We discuss open issues such as dependencies and repository consistency. We explain limitations of the current prototype and we give a perspective towards a more robust solution.

One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been verified. It appears, however, that maintaining such a repository is as hard as building it – especially for an open collection with a large number of contributors. In this paper we argue that even careful reviewing of contributions cannot cope with the task of keeping a mathematical repository efficient and clearly arranged in the long term. We discuss reasons for revisions of mathematical repositories accomplished by the “core implementors” and illustrate our experiences with revisions of MML, the Mizar Mathematical Library.