Dagstuhl Seminar 09471
Computer-assisted proofs – tools, methods and applications
( Nov 15 – Nov 20, 2009 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/09471
Organizers
- B. Malcolm Brown (Cardiff University, GB)
- Erich Kaltofen (North Carolina State University - Raleigh, US)
- Shin'ichi Oishi (Waseda University - Tokyo, JP)
- Siegfried M. Rump (TU Hamburg-Harburg, DE)
Contact
Our seminars on computer-assisted proofs are intended to assemble a diverse group of scientists working on differing aspects of computer-assisted proofs and verification methods. The current one is the fifth initiated by Rump.
Computer-assisted proofs in general are characterized by the fact that part of a mathematical proof is assisted in an algorithmic way. This includes numerical calculations, taking account of all numerical errors, as well as symbolic computations.
This concept of computer-assisted proofs can be regarded as a special approach to constructive mathematics. In recent years, various mathematical problems have been solved by computer-assisted proofs, among then the Kepler conjecture (a 3 dimensional sphere packing problem), the existence of chaos, the existence of the Lorenz attractor, and more.
This concept of computer assisted proofs can be regarded as a special approach to constructive mathematics. In recent years, various mathematical problems have been solved by computer-assisted proofs, among then the Kepler conjecture (a 3 dimensional sphere packing problem), the existence of chaos, the existence of the Lorenz attractor, and more.
A major representative of computer-assisted proofs are so-called verification methods. These are algorithms verifying the correctness of the assumptions of mathematical theorems with rigor. These methods use solely floating-point arithmetic estimating all numerical errors. Therefore these methods are particularly fast. Besides the conference, a 163-page review article on verification methods by Rump was discussed which appeared in 2010 in Acta Numerica.
The organizers refrained from presenting talks to give more space to the participants. As always, they and the 46 participants from 10 different countries of the seminar enjoyed the pleasant and stimulating atmosphere in Dagstuhl. Our own assessment is that computer-assisted proofs have several new exciting directions pursued by a number of established and young researchers, and we are already looking forward to the next seminar.
- Balazs Banhelyi (University of Szeged, HU)
- Henning Behnke (TU Clausthal, DE) [dblp]
- B. Malcolm Brown (Cardiff University, GB)
- Florian Bünger (TU Hamburg-Harburg, DE) [dblp]
- George Constantinides (Imperial College London, GB) [dblp]
- George F. Corliss (Marquette University - Milwaukee, US) [dblp]
- Tibor Csendes (University of Szeged, HU) [dblp]
- Ferenc Domes (Universität Wien, AT)
- Andreas Frommer (Bergische Universität Wuppertal, DE) [dblp]
- Stef Graillat (UPMC - Paris, FR) [dblp]
- Viktor Härter (TU Hamburg-Harburg, DE)
- Vu Hoang (KIT - Karlsruher Institut für Technologie, DE)
- Fabienne Jézéquel (Université Paris VI, FR)
- Erich Kaltofen (North Carolina State University - Raleigh, US) [dblp]
- Ralph Baker Kearfott (Univ. of Louisiana - Lafayette, US)
- Michel Kieffer (INRIA Parietal - Gif-sur-Yvette, FR)
- Kenta Kobayashi (Kanazawa University - Ishikawa-ken, JP)
- Werner Krandick (Drexel Univ. - Philadelphia, US)
- Matthias Langer (The University of Strathclyde - Glasgow, GB)
- Philippe Langlois (Université de Perpignan, FR) [dblp]
- Wen-shin Lee (University of Antwerp, BE) [dblp]
- Wolfram Luther (Universität Duisburg-Essen, DE) [dblp]
- Kaori Nagatou (Kyushu University, JP)
- Mitsuhiro T. Nakao (Kyushu University - Fukuoka, JP) [dblp]
- Arnold Neumaier (Universität Wien, AT) [dblp]
- Takeshi Ogita (Tokyo Woman's Christian University, JP) [dblp]
- Shin'ichi Oishi (Waseda University - Tokyo, JP) [dblp]
- Katsuhisa Ozaki (Waseda University - Tokyo, JP) [dblp]
- Clement Pernet (Université Joseph Fourier, FR)
- Michael Plum (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- John D. Pryce (Swindon - Wiltshire, GB) [dblp]
- Stefan Ratschan (Academy of Science - Prague, CZ) [dblp]
- Andreas Rauh (Universität Rostock, DE)
- Nathalie Revol (ENS - Lyon, FR) [dblp]
- Dagmar Roth (KIT - Karlsruher Institut für Technologie, DE)
- Siegfried M. Rump (TU Hamburg-Harburg, DE) [dblp]
- Mohab Safey El Din (UPMC - Paris, FR) [dblp]
- Hermann Schichl (Universität Wien, AT)
- Stefan Schirra (Universität Magdeburg, DE)
- Christoph Spandl (Universität der Bundeswehr - München, DE)
- Bernd Tibken (Universität Wuppertal, DE)
- Takuya Tsuchiya (Ehime University - Matsuyama, JP)
- Christian Wieners (KIT - Karlsruher Institut für Technologie, DE)
- Ian Wood (University of Kent, GB)
- Naoya Yamanaka (Waseda University - Tokyo, JP)
- Zhengfeng Yang (East China Normal University - Shanghai, CN)
- Lihong Zhi (MMRC - Beijing, CN) [dblp]
Related Seminars
- Dagstuhl Seminar 05391: Algebraic and Numerical Algorithms and Computer-assisted Proofs (2005-09-25 - 2005-09-30) (Details)
Classification
- verification / logic
- semantics / formal methods
Keywords
- Computer-assisted proofs
- verification methods
- error-free transformations
- computer algebra
- semidefinite programming
