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. |
|
Go Back |
