Mathematics: The Technology of Reasoning
Bruno Buchberger
Buchberger@RISC.Uni-Linz.ac.at
Research Institute for Symbolic Computation
Department of Mathematics and Computer Science
Johannes Kepler University
A4040 Linz,
Austria
Abstract
An exploration situation in mathematics is characterized by
- 'complete' knowledge K about a bunch of 'known' concepts (that constitute
an 'area' of mathematics) and
- a few formulae A (axioms, definitions) that describe the relation between
the new concepts and the known concepts.
The goal is 'complete' exploration of the new concepts, i.e. to conjecture
and prove / disprove formulae that describe 'all possible' interactions
between the new and the known concepts. 'Complete' knowledge about a bunch
of mathematical concepts tends to make problem solving in the respective
area 'easy', in typical cases 'algorithmic', i.e. machine-executable.
In the talk we describe the Theorema system that gives the user support in
all phases of exploration:
- formulation and manipulation of mathematical knowledge, axioms,
definitions, conjectures in a coherent (higher order predicate) logic language
- generation of mathematical proofs / refutations of conjectures using
various general and special automated provers that produce human-readable,
well-structured proofs / refutations in natural language(s)
- formulation of algorithms (special theorems that use only algorithmic
constructs of the underlying logic language) and execution of such
algorithms on input data.
Thus, Theorema provides a coherent logic and software frame for math
research, teaching, and application. Theorema is based on Mathematica and
is, hence, available on all platforms.
In the conclusion, we will give some comments about the impact of
mathematical software systems on the future of mathematics research,
teaching and application.
© 1999. ATCM, Inc.