Personalizing Mathematical Textbooks

[gusl]

from http://www.cee.hw.ac.uk/~fairouz/automath2002/abstracts/abstracts.html

Abstract: Personalizing Mathematical Textbooks
Ingo Dahn
Mathematical documents are usually well structured. They develop complex networks of concepts which are interrelated in various ways. To understand a certain mathematical theorem or example, the reader usually has to understand the environment in which it is stated. She has to understand the required definitions and the other theorems and lemmas that are eventually applied to explain it. Therefore, in different situations, different parts from a mathematical document are needed, which are frequently scattered over a large textbook. It will be shown in the talk, how Slicing Book Technology can support the reader in various such situations. This technology decomposes books into semantic units. Then the conditions under which these units can be reused are described by meta data. Automated inference procedures combine these meta data with declarative descriptions of intended documents and with information about the user to determine, how the document for the specific needs of the user should be composed. Based on this information, the document will be generated on the fly and delivered over the Web. This concept has been realized in the European project Trial-Solution (http://www.trial-solution.de) for several mathematical textbooks. We shall report on the experience gained in this project. Special attention will be paid to the implemented meta data system and how it is applied to combine content from different books for the benefit of the reader. Based on experience from the German project In2Math(http://www.uni-koblenz.de/ag-ki/PROJECTS/in2math/), an outlook will discuss the possibilities that arise when formalized mathematical objects are available as content descriptive meta data in Slicing Book Technology. Examples and demos are available from http://www.slicing.de/books/.

--------------------------------------------------------------------------------


Abstract: Theorema: A System for the Working Mathematician
Tudor Jebelean, Bruno Buchberger,
RISC-Linz, URL: www.theorema.org (paper)
The main goal of the Theorema project (Supported by Austrian Forschungsfoerderungsfonds (FWF), project P10002-PHY.) is to deliver an integrated interactive environment which can assist the mathematician in all the phases of his scientific work: proving, computing and solving in various mathematical domains. The system is implemented on top of Mathematica, thus it is backed by the full algorithmic and computing power of the currently most popular computer algebra system, which is available on all the main computing platforms (Unix, Linux, Windows, and Apple). The current implementation is the result of several man-years of work by many people of the \tma\ group at RISC, under the direction of Bruno Buchberger. Until now, we already built into the system the main features concerning proving and computing, while the solving features are in the design phase. The main features of the system will be demonstrated live during this presentation.

The system interacts with the user in the language of predicate logic, which is the natural language for expressing mathematical properties and algorithms. Few intuitive commands allow the user to enter mathematical formulae (in natural two-dimensional notation) and to compose them into mathematical theories, and also to use some basic domains (numbers, tuples, sets) which are already provided in Theorema Moreover, the system provides the implementation of the powerfull concept of {\em functor}, which allows the build-up of sophisticated domains on top of simpler ones. The mathematician has the possibility to experiment with the algorithms expressed in this way by directly running them using the Theorema computing engine, and he can also study their formal properties (e.g. correctness) using the {\em provers} of Theorema. It is an unique feature of Theorema that these two phases of the mathematical activity can be performed in the same integrated system and using the same language.

Computation is performed under full control of the user, which means being able to trace the reason (definition, formula) for each computing step -- if necessary, but most important with full control of the {\em knowledge} which is used in the computing process. For instance, in a certain situation the mathematician wants to give to the symbols (*, +, 0, Successor) the axiomatic meaning as defined by induction over natural numbers, while in another situation the same symbols should be interpreted using the full power of the underlying computational engine (positional notation, long arithmetic, etc.)

Proving is done with specific methods for several mathematical domains: propositional logic, general predicate logic, induction over integers and over lists, set theory, boolean combinations of polynomial [in]equalities (using Groebner Bases), combinatorial summation (using Paule--Schorn--Zeilberger), and a novel technique for proving in higher-order logic with equality: PCS (proving--computing--solving), introduced by Buchberger.

Theorema departs from the methods mostly used in automatic provers today, because it uses a natural proving style: the formulae are expressed in their original form (two-dimensional, non-clausal), the inference steps are expressed in natural style and in human language, and -- most importantly -- the proving methods are similar to the ones which are used by the working mathematicians. Therefore, the user has the possibility to inspect and easily understand the proofs, to verify any inference, and to interact with the proof by modifying certain assumptions, etc.


--------------------------------------------------------------------------------


Abstract:On the Design of Mathematical Concepts
Manfred Kerber
The insight that foundational systems like first-order logic or set theory can be used to construct large parts of existing mathematics and formal reasoning is one of the deep mathematical insights. Unfortunately it has been used in the field of automated theorem proving as an argument to disregard the need for a diverse variety of approaches in the field. While design issues play a major role in the formation of mathematical concepts, the theorem proving community has largely neglected them. In this contribution we argue that this leads not only to problems at the human computer interaction end, but that it causes severe problems at the core of the systems, namely at their representation and reasoning capabilities. (joint work with Martin Pollet of Saarbruecken, Germany.)

Comments

[jcreed.livejournal.com]

Damn! The book with all these papers in it was only published two months ago, so it's not in any libraries around here. It all looks like really cool stuff.