Recently, a number of problems have been solved by so-called computer-assisted proofs, among them the celebrated Kepler conjecture, the proof of existence of chaos, the verification of the existence of the Lorenz attractor, and more. All those problems have two things in common: first, the computer is used to assist the proof by solving certain subproblems, and second these subproblems are of numerical nature.
There are also any famous results of nontrivial proofs which can be performed automatically by a computer program. For example, Risch's algorithm for integration in finite terms, solution of polynomial systems by Gröbner bases, quantifier elimination and more. Any of those solves a nontrivial mathematical problem which could be quite hard to solve by pencil and paper.
Those algorithms are frequently executed in exact arithmetic over the field of rationals or an algebraic extension field using well known methods from computer algebra. The problems mentioned in the first paragraph are continuous in nature. Tehy can be solved by so-called verification or self-validating methods.
Basically, self-validating methods verify the validity of assertions of certain theorems which are formulated in such a way that validation is possible by means of numerical computations. The main point is that this validation is absolutely rigorous including all possible procedural or rounding errors. On the one hand, the use of finite precision arithmetic implies very fast calculations, but on the other hand it limits the scope of applicability.
In contrast, most algorithms in computer algebra are 'never failing', that is they are proved to provide a solution for any input, and the maximum computing time for this is estimated a priori. To speed up practical implementations, also hybrid methods combining computer algebra with numerical verification methods are used.
Self-validating and computer algebra methods aim on the reliable solution of certain mathematical problems with the aid of computers. This seems a very natural task. Other areas such as computer geometry and graphics, real number theory, automated theorem proving and more have similar aims. Therefore we think it is very fruitful to create a link of information between experts in those different fields. The common basis or goal is the computer-assisted solution of mathematical problems with certainty.
The choice of organizers also reflects different fields of interest and expertise. The stimulating atmosphere in Dagstuhl was definitely a very fruitful environment for this enterprise.
- Götz Alefeld (KIT - Karlsruher Institut für Technologie, DE)
- Hirokazu Anai (Fujitsu Laboratories - Kawasaki, JP)
- Balazs Banhelyi (University of Szeged, HU)
- Prashant Batra (TU Hamburg-Harburg, DE)
- Henning Behnke (TU Clausthal, DE) [dblp]
- Sylvie Boldo (University of Paris South XI, FR) [dblp]
- Bruno Buchberger (Universität Linz, AT)
- Jean-Marie Chesneaux (UPMC - Paris, FR)
- George F. Corliss (Marquette University - Milwaukee, US) [dblp]
- Tibor Csendes (University of Szeged, HU) [dblp]
- Luiz Henrique de Figueiredo (IMPA - Rio de Janeiro, BR)
- Borbála Fazekas (KIT - Karlsruher Institut für Technologie, DE)
- Andreas Frommer (Bergische Universität Wuppertal, DE) [dblp]
- Stef Graillat (Université de Perpignan, FR) [dblp]
- Olga Holtz (University of California - Berkeley, US)
- Christian Jansson (TU Hamburg-Harburg, DE)
- Christian Keil (TU Hamburg-Harburg, DE)
- Kenta Kobayashi (Kyushu University, JP)
- Philippe Langlois (Université de Perpignan, FR) [dblp]
- Wolfram Luther (Universität Duisburg-Essen, DE) [dblp]
- Nami Matsunaga (Waseda Univ. / JST - Tokyo, JP)
- Kurt Mehlhorn (MPI für Informatik - Saarbrücken, DE) [dblp]
- Kaori Nagatou (Kyushu University, JP)
- Mitsuhiro T. Nakao (Kyushu University, JP) [dblp]
- Arnold Neumaier (Universität Wien, AT) [dblp]
- Takeshi Ogita (Waseda Univ. / JST - Tokyo, JP) [dblp]
- Shin'ichi Oishi (Waseda Univ. / JST - Tokyo, JP) [dblp]
- Knut Petras (Bergische Universität Wuppertal, DE)
- Michael Plum (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Stefan Ratschan (Academy of Science - Prague, CZ) [dblp]
- Markus Rosenkranz (RICAM - Linz, AT)
- Stefan Schirra (Universität Magdeburg, DE)
- Stephan Schulz (TU München, DE) [dblp]
- Eric Walter (Supélec - Gif-sur-Yvette, FR)
- Yoshitaka Watanabe (Kyushu University, JP)
- Freek Wiedijk (Radboud University Nijmegen, NL) [dblp]
- Christian Wieners (KIT - Karlsruher Institut für Technologie, DE)
- Nobito Yamamoto (The University of Electro-Communications - Tokyo, JP) [dblp]
- Kazuhiro Yokoyama (Rikkyo University - Tokyo, JP) [dblp]
- Dagstuhl Seminar 09471: Computer-assisted proofs - tools, methods and applications (2009-11-15 - 2009-11-20) (Details)