Computer-Assisted Proofs and Verification Methods
- Time: 18.9.2011 - 22.9.2011
September 18 - 22, 2011
Location — Organizers — Schedule — Speakers
The 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 them the Kepler conjecture (a 3-dimensional sphere packing problem), the existence of chaos, the existence of the Lorenz attractor, and more.
In the SIAM News 1-2/2002, Lloyd N. Trefethen (Oxford) proposed a 10x10 digit Challenge. These are ten difficult numerical problems with a single number as result. The problems vary from global optimization, numerical integration, partial differential equations to probabilistic problems and more. The challenge was to produce 10 correct digits of each solution. Various researchers participated in the contest, but only few of them could give correct answers. An outstanding approach, winning the contest, was the result of effort by a group of four researchers from four different countries. Remarkably, five out of the ten problems were solved using verification methods and the MATLAB toolbox INTLAB for reliable computing developed by S.M. Rump (TU Hamburg-Harburg).
Many problems involving partial differential equations, with a huge number of applications in science and engineering, allow very stable numerical computations of approximate solutions, but are still lacking analytical existence and multiplicity proofs. In recent years, methods have been developed which supplement purely analytical arguments by computer-assisted approaches, and these methods have turned out to be successful in various examples where purely analytical methods have failed. One of the organizers (Plum) and the Japanese scientists M.T. Nakao and S. Oishi have made internationally recognized contributions by computer-assisted proofs in the field of partial differential equations and their applications, like fluid dynamics (Navier-Stokes problems, Orr-Sommerfeld equation, Rayleigh-Benard heat convection), electro-dynamics (photonic crystals, scattering problems described by the Lippmann Schwinger equation), magneto-hydrodynamics (plasma flow), nonlinear waves (for example, travelling waves in a beam), elasticity/plasticity, variational inequalities, obstacle problems, and semilinear elliptic boundary and eigenvalue problems in general. In this context, various kinds of constants appearing e.g. in finite element error bounds or in Sobolev embeddings are needed explicitly, and have been determined by computations of analytical and computer-assisted means.
S.M. Rump and S. Oishi have extensively developed arithmetic and linear algebra tools for computer assisted proofs based on numerical computations with guaranteed accuracy. For example, they have developed fast and ultra-fast methods for solving numerical linear algebraic problems with guaranteed accuracy, adaptive methods for solving ill-posed problems in numerical linear algebra, accurate summation and dot product algorithms for floating point vectors. These methods are also provided in the aforementioned MATLAB interval toolbox INTLAB for verification algorithms, which is widely used all over the world. As an application of these tools, Oishi and Rump have also developed algorithms in computational geometry, which always give mathematically correct results even if they are executed by floating point calculations.
The particular expertise of Japanese and German scientists indicates that a workshop with participants primarily from Japan and Germany and from all the described subareas will be very promising. We are convinced that our workshop has high potential for very fruitful interactions between these areas. Moreover, it will lead to significant developments in several inter-related fields like numerical functional analysis, ordinary and partial differential equations, ill-posed and ill-conditioned problems, constrained programming, reliable algorithms, and topics related to computer arithmetic.
Location Kaiserstraße 93, Rooms 1C-04, 1C-01 - Please see map!
Organizers G. Alefeld (Karlsruhe), M. Plum (Karlsruhe), S. M. Rump (Hamburg-Harburg)
- Henning Behnke, Computer Assisted Enclosures for Sloshing Frequencies
- Florian Bünger, A Numerical Verification Method for the Existence and Uniqueness of Solutions of Non-Linear Second Order Sturmian Boundary Value Problems
- Andreas Frommer (and Behnam Hashemi), Computational Proofs of the Stability of Lyapunov Equations
- Christian Jansson, Optimization with Guaranteed Accuracy: Application and Software
- Walter Krämer, Arbitrary Complex Interval Functions
- Xuefeng Liu(and Shinchi'ichi Oishi), On Computable Eigenvalue Evaluation for Elliptic Eigenproblem with Singularity
- Günter Mayer, On the Semiconvergence of Powers of Interval Matrices
- Mitsuhiro T. Nakao, On the Verified Computation of Solutions for Parabolic Initial-Boundary Value Problems
- Shin'ichi Oishi (and Akitoshi Takayasu, Xuefeng Liu), Numerical Existence test for Solutions of Nonlinear Elliptic Equation on Bounded Nonconvex Polyhedral Domain
- Katsuhisa Ozaki, Best Accuracy of Matrix Multiplication by Error-Free Transformation with Level 3 BLAS
- Dagmar Roth, A Computer-Assisted Multiplicity Proof for a Semilinear Elliptic Boundary Value problem
- Yoshitaka Watanabe, A Computer-Assisted Proof for Functional Equations Based on Infinite Dimensional Sequential Iteration
- Nobito Yamamoto (and Masato Harikae), Validated Computation of Global Solutions to ODEs