Computer Science Logic and 8th Kurt Gödel Colloquium
Bruno Buchberger: Computational Mathematics, Computational Logic, and Symbolic Computation
Welcome and News
Host Institutions
Calls and Deadlines
Program
Social Program
Registration
Location and Venue
Accommodation
Committees
Contact
Colocated Events
Authors' instructions
Print current pagePrint this page
``Computational mathematics'' (algorithmic mathematics) is the part of mathematics that strives at the solution of mathematical problems by algorithms. In a superficial view, some people might believe that computational mathematics is the easy part of mathematics in which trivial mathematics is made useful by repeating trivial steps sufficiently many times on current powerful machines in order to achieve marginally interesting results. The opposite is true: Many times, computational mathematics needs and stimulates deeper mathematics, i.e. deeper mathematical theorems with more difficult proofs than ``pure'' mathematics. This is so because, in order to establish an algorithmic method for a given mathematical problem, i.e. in order to reduce the solution of a given problem to the few operations that can be executed on machines, deeper insight on the given problem domain is necessary than the insight necessary for establishing the reduction of the given problem to powerful nonalgorithmic abstract mathematical operations as, for example, choice functions and the basic quantifiers of set theory.

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 non-trivial 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 meta-theory of mathematics. The characteristic feature of mathematics is its method of gaining knowledge from given knowledge by reasoning. Hence, the meta-theory 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 meta-level 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 meta-level 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 meta-level. 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.


© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-09 Valid HTML 4.01! Valid CSS! Debian