Theory Exploration with Theorema
Bruno Buchberger
In: Proceedings of SYNASC 2000 (2nd International Workshop on Symbolic
and Numeric Algorithms in Scientific Computing), Oct. 4-6,
2000, Timisoara, Rumania, (T. Jebelean, V. Negru, A. Popovici eds.),
Analele Universitatii Din Timisoara, Ser. Matematica-Informatica,
Vol. XXXVIII, Fasc.2, 2000, pp. 9-32.
(ISSN 1124-970X. Copyright: University of the West at Timisora.)
ABSTRACT:
We introduce the paradigm of computer-supported theory exploration
and propose it as a more attractive alternative to the traditional paradigm
of automated theorem proving. We characterize exploration situations by
- a collection of known concepts
- a collection of facts about the known concepts
- a new concept
- axioms that relate the new concept with the known concepts
- a collection of goal propositions that "completely" explore the relation
between the new concept and the known concepts.
We analyze the notion of "complete" knowledge and propose two approaches
for the complete exploration of new concepts.
By going through a couple of exploration rounds, mathematical exploration
arrives at higher and higher layers of knowledge. In the transition to
higher layers, it is often useful to condense special knowledge into the form
of special proof techniques. This paradigm of "transition from knowledge to
inferencing" seems to be a fundamental principle that made human proving
successful and feasible in the systematic build-up of mathematics.
We illustrate the general philosophy of theory exploration by examples in the
frame of the Theorema software system currently developed by the Theorema
Group under the direction of the author.