This document is better viewed as Mathematica notebook.
If you do not have an installation of Mathematica 3.0, then you can
download MathReader (http://www.wri.com/mathreader) free of charge.
==========================================
Title
============
Theory Exploration Versus Theorem Proving
Author
============
Bruno Buchberger
Abstract
============
The Theorema system is a system for proving, solving, and simplifying mathematic
al formulae.
It is programmed in the Mathematica language, version 3.0 or later, and also hea
vily uses
the front-end of Mathematica. Theorema can therefore be used on all machines on
which Mathematica,
version 3.0 or later, is installed.
In normal math research, teaching, and application, we do not consider individua
l theorems.
Rather, we explore an entire 'theory', i.e.:
- we proceed in proving 'layers' of more and more complex propositions;
- in each layer, we consider (try to prove or disprove)
the propositions as an ensemble and not isolated;
- in each layer, we prove by reduction to the (immediately) preceding layer(s)
and not by reduction to 'first principles'.
The thesis of this paper:
- Organized theory exploration instead of isolated theorem proving has a drastic
influence on the feasibility, power, naturalness and practical attractiveness
of
automated theorem proving.
- Hence, future mathematical software systems that integrate theorem proving sho
uld
support theory generation in various ways.
==========================================