Catálogo de publicaciones - libros

In Section 15.6 we have presented a notion of theory and inheritance that is sufficient for simple applications like content dictionaries that informally (though presumably rigorously) define the static meaning of symbols. Experience in e.g. program verification has shown that this infrastructure is insufficient for large-scale developments of formal specifications, where reusability of formal components is the key to managing complexity. For instance, for a theory of rings we cannot simply inherit the same theory of monoids as both the additive and multiplicative structure.

In this chapter, we will generalize the inheritance relation from Section 15.6 to that of “theory inclusions”, also called “theory morphisms” or “theory interpretations” elsewhere [Far93]. This infrastructure allows to structure a collection of theories into a complex theory graph that particularly supports modularization and reuse of parts of specifications and theories. This gives rise to the name “complex theories” of the module.

As we have seen, is concerned mainly with the content and structure of mathematical documents, and offers a complex infrastructure for dealing with that. However, mathematical texts often carry typographic conventions that cannot be determined by general principles alone. Moreover, non-standard presentations of fragments of mathematical texts sometimes carry meanings that do not correspond to the mathematical content or structure proper. In order to accommodate this, provides a limited functionality for embedding style information into the document.

Up to now, we have been mainly concerned with providing elements for marking up the inherent structure of mathematical knowledge in mathematical statements and theories. Now, we interface documents with the Internet in general and mathematical software systems in particular. We can thereby generate presentations from documents where formulae, statements or even theories that are active components that can directly be manipulated by the user or mathematical software systems. We call these documents . For this we have to solve two problems: an abstract interface for calls to external (web) services and a way of storing application-specific data in documents (e.g. as arguments to the system calls).

The module EXT provides a basic infrastructure for these tasks in . The main purpose of this module is to serve as an initial point of entry. We envision that over time, more sophisticated replacements will be developed driven by applications.

Exercises and study problems are vital parts of mathematical documents like textbooks or exams, in particular, mathematical exercises contain mathematical vernacular and pose the same requirements on context like mathematical statements. Therefore markup for exercises has to be tightly integrated into the document format, so provides a module for them.

Note that the functionality provided in this module is very limited, and largely serves as a place-holder for more pedagogically informed developments in the future (see Section 26.8 and [GMUC03] for an example in the framework).

In almost all XML applications, there is a tension between the document view and the object view of data; after all, XML is a document-oriented interoperability framework for exchanging data objects. The question, which view is the correct one for XML in general is hotly debated among XML theorists. In , actually both views make sense in various ways. Mathematical documents are the objects we try to formalize, they contain knowledge about mathematical objects that are encoded as formulae, and we arrive at content markup for mathematical documents by treating knowledge fragments (statements and theories) as objects in their own right that can be inspected and reasoned about.

In Chapters 13 to 21, we have defined what documents look like and motivated this by the mathematical objects they encode. But we have not really defined the properties of these documents as objects themselves (we will speak of the (OMDOM)). To get a feeling for the issues involved, let us take stock of what we mean by the object view of data. In mathematics, when we define a class of mathematical objects (e.g. vector spaces), we have to say which objects belong to this class, and when they are to be considered equal (e.g. vector spaces are equal, iff they are isomorphic). When defining the intended behavior of operations, we need to care only about objects of this class, and we can only make use of properties that are invariant under object equality. In particular, we cannot use properties of a particular realization of a vector space that are not preserved under isomorphism. For document models, we do the same, only that the objects are documents.

In this part we will address current applications, tools and projects using the format. We will first discuss the possibilities and tools of processing documents in the format via style sheets with the purpose of generating documents specialized for consumption by other mathematical software systems, and by humans. Then we will present three projects descriptions that use at the core.

In this chapter we will describe various public resources for working with the format.

In Chapter 1 we have briefly discussed the basics of validating XML documents by document type definitions (DTDs) and schemata. In this chapter, we will instantiate this discussion with the particulars of validating documents.

Generally, DTDs and schemata are context-free grammars for trees, that can be used by a to reject XML documents that do not conform to the constraints expressed in the DTD or schemata discussed here.

Note that none of these grammars can enforce all constraints that the specification in Part III of this book imposes on documents. Therefore grammar-based validation is only a necessary condition for -. Still, documents should be validated to ensure proper function of tools, such as the ones discussed in Chapters 25 and 26. Validation against multiple grammars gives the best results. With the current state of validation technology, there is no clear recommendation, which of the validation approaches to prefer for . DTD validation is currently best supported by standard XML applications and supports default values for attributes. This allows the author who writes documents by hand to elide implicit attributes and make the marked-up text more readable. XML- and schema validation have the advantage that they are namespace-aware and support more syntactic constraints. Neither of these support mnemonic XML entities, such as the ones used for characters in Presentation-, so that these have to be encoded as code points. Finally schemata do not fully support default values for attributes, so that documents have to be normalized to be -valid.

We will now discuss the particulars of the respective validation formats. As the schema is the most expressive and readable for humans we consider it as the normative grammar formalism for , and have included it in Appendix D for reference.

In the introduction we have stated that one of the design intentions behind is to separate content from presentation, and leave the latter to the user. In this section, we will briefly touch upon presentation issues. The technical side of this is simple: documents are regular XML documents that can be processed by XSLT style sheets [XSL99] to produce the desired output formats. There are several high-quality XSLT transformers freely available including  [Kay],  [Fou], and  [Veib]. Moreover, XSLT is natively supported by the newest versions of the browsers MS Internet Explorer [Cor] and  [Org].

XSLT style sheets can be used for several tasks in maintaining , such as for instance converting other XML-based input formats into (e.g. for converting content dictionaries into format), or migrating between different versions of e.g. the style sheet that operationalizes all the syntax changes from Version 1.1 to version 1.2 (see Appendix A for a tabulation). We will now review a set of XSLT style sheets for , they can be found in the distribution (see Section 23.2) or on the web at [Kohg].

This chapter presents a variety of applications and projects that use the format or are related to it in a substantive way.

Apart from the projects directly reported here, the format is used by the new research field of Mathematical Knowledge Management (; cf. ), which combines researchers in mathematics, computer science, and library science. We refer the reader to the proceedings of the annual conference [BC01b, Asp03, ABT04, Koh05b, BF06].