Bruno Buchberger: Computational Mathematics, Computational Logic, and Symbolic Computation  

Computational mathematics comes in two flavors: ``numerical mathematics'', in which the original problems are replaced by approximate versions and one is satisfied with approximate solutions to the approximate problems, and ``exact algorithmic mathematics'' in which the original problems are solved by algorithms in the original domains or isomorphic representations of these domains. Exact algorithmic mathematics can be divided into ``discrete mathematics'', in which the objects in the underlying mathematical domains are finitary, and ``computer algebra'', in which the objects in the underlying mathematical domains according to their original defintion are infinite and the possibility of an isomorphic finitary representation in itself is a nontrivial mathematical question. For many mathematical problems it can be mathematically proved that exact algorithmic solutions are not possible or are possible only by algorithms with a certain complexity. Even in these cases, algorithmic mathematics can and should go on by considering either approximate versions or special cases of the problem. Mathematical logic is the mathematical metatheory of mathematics. The characteristic feature of mathematics is its method of gaining knowledge from given knowledge by reasoning. Hence, the metatheory of mathematics is essentially the theory of reasoning. As any other mathematical theory, one can and should ask the question of how much of reasoning can be made algorithmic. The part of mathematical logic that deals with algorithmic methods for reasoning is called ``computational logic''. Although it is well known that the algorithmization of mathematical reasoning in its most general form in a certain sense is not possible, the algorithmization of reasoning under certain restrictions or for certain limited  but still extremely broad  areas of mathematics is possible and, in fact, is one of the most challenging mathematical endeavors with enormous practical significance. In fact, as a result of analyzing mathematical invention in the various areas of mathematics, it turns out that the transition from the object level to the metalevel is not limited to mathematical logic but is one of the main  but mostly hidden  instruments of mathematical progress in every field of mathematics and at the core of mathematical intelligence and invention. We therefore advocate that future mathematical systems must provide a frame for considering both the object and the metalevel of mathematical theories and must provide a means for the transition from the object level to the metalevel. In fact, ``symbolic computation'' is a term that more and more is used as a common term for both computer algebra flavored computational mathematics on the object level and computational logic on the metalevel. In other words, ``symbolic computation'' grows into the most general frame for all aspects of algorithmization. More concretely, in the recent research efforts of the symbolic computation community, the interaction of computer algebra and computational logic and the applications of the results of this interaction for the future automation of ``mathematical knowledge management'' moves into the center of interest. In the talk, we will illustrate the above general outline by examples of symbolic computation algorithms and its underlying theories and by some demos in the Theorema software system.
