Catálogo de publicaciones - libros

can be used as content language for communication protocols between mathematical software systems on the Internet. The ability to specify the context and meaning of the mathematical objects makes the format ideally suited for this task.

In this chapter we will discuss a message interface in a fictitious software system , which connects a wide-range of reasoning systems (), such as automated theorem provers, automated proof assistants, computer algebra systems, model generators, constraint solvers, human interaction units, and automated concept formation systems, by a common . Reasoning systems integrated in can therefore offer new services to the pool of services, and can in turn use all services offered by other systems.

The (pen athematical uments) format is a content markup scheme for (collections of) mathematical documents including articles, textbooks, interactive books, and courses. also serves as the content language for agent communication of mathematical services on a mathematical software bus.

This part of the book is the specification of version 1.2 of the format, the final and mature release of version 1. It defines the language features and their meaning. The content of this part is normative for the format; an document is valid as an document, iff it meets all the constraints imposed here. applications will normally presuppose valid documents and only exhibit the intended behavior on such.

A modular approach to design is generally accepted as best practice in the development of any type of complex application. It separates the application’s functionality into a number of “building blocks” or “modules”, which are subsequently combined according to specific rules to form the entire application. This approach offers numerous advantages: The increased conceptual clarity allows developers to share ideas and code, and it encourages reuse by creating well-defined modules that perform a particular task. Modularization also reduces complexity by decomposition of the application’s functionality and thus decreases debugging time by localizing errors due to design changes. Finally, flexibility and maintainability of the application are increased because single modules can be upgraded or replaced independently of others.

The vocabulary has been split by thematic role, which we will briefly overview in Figure 10.1 before we go into the specifics of the respective modules in Chapters 13 to 21. To avoid repetition, we will introduce some attributes already in this chapter that are shared by elements from all modules. In Chapter 22 we will discuss the document model and possible sub-languages of that only make use of parts of the functionality (Section 22.3).

The first four modules in Figure 10.1 are required (mathematical documents without them do not really make sense), the other ones are optional. The document-structuring elements in module DOC have an attribute that allows to specify which of the modules are used in a particular document (see Chapter 11 and Section 22.3).

Mathematical knowledge is largely communicated by way of a specialized set of documents (e.g. e-mails, letters, pre-prints, journal articles, and textbooks). These employ special notational conventions and visual representations to convey the mathematical knowledge reliably and efficiently.

When marking up mathematical knowledge, one always has the choice whether to mark up the structure of the document itself, or the structure of the mathematical knowledge that is conveyed in the document. Even though in most documents, the document structure is designed to help convey the structure of the knowledge, the two structures need not be the same. To frame the discussion we will distinguish two aspects of mathematical documents. In the we organize the mathematical knowledge by its function, and do not care about a way to present it to human recipients. In the we are interested in the structure of the argument that is used to convey the mathematical knowledge to a human user.

Metadata is “data about data” — in the case of data about documents, such as titles, authorship, language usage, or administrative aspects like modification dates, distribution rights, and identifiers. To accommodate such data, offers the element in many places. The most commonly used metadata standard is the Dublin Core vocabulary, which is supported in some form by most formats. uses this vocabulary for compatibility with other metadata applications and extends it for document management purposes in . Most importantly extends the use of metadata from documents to other (even mathematical) elements and document fragments to ensure a fine-grained authorship and rights management.

In the following we will describe the variant of Dublin Core metadata elements used in . Here, the element can contain any number of instances of any Dublin Core elements described below in any order. In fact, multiple instances of the same element type (multiple elements for example) can be interspersed with other elements without change of meaning. extends the Dublin Core framework with a set of roles (from the MARC relator set [MAR03]) on the authorship elements and with a rights management system based on the Creative Commons Initiative.

A distinguishing feature of mathematics is its ability to represent and manipulate ideas and objects in symbolic form as mathematical formulae. uses the and Content- formats to represent mathematical formulae and objects. Therefore, the standard [BCC+04] and the 2.0 recommendation (second edition) [ABC+03] are part of this specification. We will review objects (top-level element ) in Section 13.1 and Content- (top-level element ) in Section 13.2, and specify an element for entering mathematical formulae (element ) in Section 13.5.

The recapitulation in the next two sections is not normative, please consult Section 2.1 for a general introduction and history and the standard and the 2.0 Recommendation for details and clarifications.

The everyday mathematical language used in textbooks, conversations, and written onto blackboards all over the world consists of a rigorous, slightly stylized version of natural language interspersed with mathematical formulae, that is sometimes called .

In this chapter we will look at the infrastructure to mark up the of mathematical statements and their interaction with a broader mathematical context.

Most specification languages for mathematical theories support definition mechanisms for sets that are inductively generated by a set of constructors and recursive functions on these under the heading of . Prominent examples of abstract data types are natural numbers, lists, trees, etc. The module ADT presented in this chapter extends by a concise syntax for abstract data types that follows the model used in the (Common Abstract Specification Language [CoF04]) standard.

Proofs form an essential part of mathematics and modern sciences. Conceptually, a is a representation of uncontroversial evidence for the truth of an assertion.

The question of what exactly constitutes a proof has been controversially discussed (see e.g. [BC01a]). The clearest (and most radical) definition is given by theoretical logic, where a proof is a sequence, or tree, or directed acyclic graph (DAG) of applications of inference rules from a formally defined logical calculus, that meets a certain set of well-formedness conditions. There is a whole zoo of logical calculi that are optimized for various applications. They have in common that they are extremely explicit and verbose, and that the proofs even for simple theorems can become very large. The advantage of having formal and fully explicit proofs is that they can be very easily verified, even by simple computer programs. We will come back to this notion of proof in Section 17.4.

In mathematical practice the notion of a proof is more flexible, and more geared for consumption by humans: any line of argumentation is considered a proof, if it convinces its readers that it could in principle be expanded to a formal proof in the sense given above. As the expansion process is extremely tedious, this option is very seldom carried out explicitly. Moreover, as proofs are geared towards communication among humans, they are given at vastly differing levels of abstraction. From a very informal proof idea for the initiated specialist of the field, who can fill in the details herself, down to a very detailed account for skeptics or novices which will normally be still well above the formal level. Furthermore, proofs will usually be tailored to the specific characteristics of the audience, who may be specialists in one part of a proof while unfamiliar to the material in others. Typically such proofs have a sequence/tree/DAG-like structure, where the leaves are natural language sentences interspersed with mathematical formulae (or mathematical vernacular).