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.


==========================================