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.