TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 09471

Computer-assisted proofs – tools, methods and applications

( 15. Nov – 20. Nov, 2009 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/09471

Organisatoren



Summary

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.


Teilnehmer
  • 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 A. 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]

Verwandte Seminare
  • Dagstuhl-Seminar 05391: Algebraic and Numerical Algorithms and Computer-assisted Proofs (2005-09-25 - 2005-09-30) (Details)

Klassifikation
  • verification / logic
  • semantics / formal methods

Schlagworte
  • Computer-assisted proofs
  • verification methods
  • error-free transformations
  • computer algebra
  • semidefinite programming