Catálogo de publicaciones - libros

Capturing and understanding mathematics from print form is an important task in translating written mathematical knowledge into electronic form. While the problem of syntactically recognising mathematical formulas from scanned images has received attention, very little work has been done on semantic validation and correction of recognised formulas. We present a first step towards such an integrated system by combining the system with a semantic analyser for matrix expressions. We applied the combined system in experiments on the semantic analysis of matrix images scanned from textbooks. While the first results are encouraging, they also demonstrate many ambiguities one has to deal with when analysing matrix expressions in different contexts. We give a detailed overview of the problems we encountered that motivate further research into semantic validation of mathematical formula recognition.

For the transfer of mathematical knowledge from paper to electronic form, the reliable automatic analysis and understanding of mathematical texts is crucial. A robust system for this task needs to combine low level character recognition with higher level structural analysis of mathematical formulas. We present progress towards this goal by extending a database-driven optical character recognition system for mathematics with two high level analysis features. One extends and enhances the traditional approach of projection profile cutting. The second aims at integrating the recognition process with graph grammar rewriting by giving support to the interactive construction and validation of grammar rules. Both approaches can be successfully employed to enhance the capabilities of our system to recognise and reconstruct compound mathematical expressions.

In this paper, we address the problem of automatic keywords assignment to scientific publications. The idea to use textual traces learned from training data in a supervised manner to identify appropriate keywords is considered. We introduce the transparent concept of identification cloud as a means to represent the semantics of scientific terms. This concept is mathematically defined by models of scientific terms stochastic distributions over publication texts. Characteristics of models as well as procedures for both non-parametric and parametric estimation of probability distributions are presented.

We present a content markup language for physics realized by extending the format by an infrastructure for the principal concepts of physics: , physical , and . The formalization of the description of physics observables follows the structural essence of the operational theory of physics measurements. The representational infrastructure for systems and experiments allow to capture the distinctive practice of physics: natural laws are supported by evidence from experiments which are described, disseminated and reproduced by others.

We explore the social context of mathematical knowledge: Even though, the community of mathematicians may look homogeneous from the outside, it is actually structured into various sub-communities that differ in preferred notations, the choice of basic assumptions, or e.g. in the choice of motivating examples. We contend that we cannot manage mathematical knowledge for human recipients if we do not take these factors into account. As a basis for a future extension of MKM systems, we analyze the social context of information in terms of Communities of Practice (CoP; a concept from learning theory) and present a concrete extensional model for CoPs in mathematics.

Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully.

In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications.

Much work in MKM depends on the application of formal logic to mathematics. However, much mathematical knowledge is informal. Luckily, formal logic only represents one tradition in logic, specifically the modeling of inference in terms of logical form. Many inferences cannot be captured in this manner. The study of such inferences is still within the domain of logic, and is sometimes called informal logic. This paper explores some of the benefits informal logic may have for the management of informal mathematical knowledge.

OpenMath is a widely recognised approach to the semantic markup of mathematics that is often used for communication between OpenMath compliant systems. The Aldor language has a sophisticated category-based type system that was specifically developed for the purpose of modelling mathematical structures, while the system itself supports the creation of small-footprint applications suitable for deployment as web services. In this paper we present our first results of how one may perform translations from generic OpenMath objects into values in specific Aldor domains, describing how the Aldor domain is used to achieve this. We outline our Aldor implementation of an OpenMath translator, and describe an efficient extension of this to the Parser category. In addition, the Aldor service creation and invocation mechanism are explained. Thus we are in a position to develop and deploy mathematical web services whose descriptions may be directly derived from Aldor’s rich type language.

The HR system forms scientific theories, and has found particularly successful application in domains of pure mathematics. Starting with only the axioms of an algebraic system, HR can generate dozens of example algebras, hundreds of concepts and thousands of conjectures, many of which have first order proofs. Given the overwhelming amount of knowledge produced, we have provided HR with sophisticated tools for handling this data. We present here the first full description of these management tools. Moreover, we describe how careful analysis of the theories produced by HR – which is enabled by the management tools – has led us to make interesting discoveries in algebraic domains. We demonstrate this with some illustrative results from HR’s theories about an algebra of one axiom. The results fueled further developments, and led us to discover and prove a fundamental theorem about this domain.

Within the project, a collection of files and supporting material has been realized. This content covers the derivative side of calculus and is being used by students in the learning environment. is the first collection trying to make use of most of the features of the learning environment including advanced usages of and . It has been written in , a readable -syntax.

This paper describes the tools to produce it, how they were used and combined, the resulting content and the experience gained. It argues that the declaration of new symbols is a requirement and explains challenges of authoring semantic mathematical content. Finally, it presents the management activities to support the authoring process.