``Mathematical Tools in Interactive Learning, a Digital Approach.''

Abstracts of the Talks

A Survey of the Theorema Project and its Applications for Interactive Textbooks in Mathematics.

Bruno Buchberger, Tudor Jebelean, Franz Kriftner
Mircea Marin, Robert Pollak, Elena Tomuta, Daniela Vasaru
Research Institute for Symbolic Computation, Linz, Austria.
Email: firstname.lastname@risc.uni-linz.ac.at

The Theorema project aims at extending current computer algebra systems by facilities for supporting mathematical proving. The present early-prototype version of the Theorema software system is implemented in Mathematica 3.0. The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language presented in nested cells. The special provers are intimately connected with the functors that build up the various mathematical domains. The long-term goal of the project is to produce a complete system which supports the mathematician in creating interactive textbooks, i.e. books containing, besides the ordinary passive text, active text representing algorithms in executable format, as well as proofs which can be studied at various levels of detail, and whose [routine] parts can be automatically generated. This system will provide a uniform (logic and software) framework in which a working mathematician, without leaving the system, can get computer-support while looping through all phases of the mathematical problem solving cycle:

the phase of specifying a problem including the compilation of relevant knowledge and the definition of new concepts (predicates, functions) and auxiliary algorithms;
the phase of exploring a given problem and creating ideas and conjectures by studying examples using the available knowledge and algorithms;
the phase of proving or disproving conjectures and thereby increasing the relevant knowledge base;
the phase of programming, i.e. transforming useful new and provenly correct mathematical knowledge into algorithms for solving the initial problem;
the phase of writing up one's finding in interactive mathematical documents.

The authors work under the direction of the first author and jointly with him on the following parts of the system: syntax of the mathematical language (F. Kriftner), predicate logic prover (T. Jebelean), inductive prover for lists (D. Vasaru), generation of knowledge bases from functors (E. Tomuta), simplification prover (M. Marin), prover for polynomials (R. Pollak).

Reference:B. Buchberger et. al. A survey on the Theorema project
In Proceedings of ISSAC'97, to appear in ACM Press, 1997.
Also available as RISC technical report 97-15, http://www.risc.uni-linz.ac.at/library/.

Go to:

List of talks

MaTILDA Home page