MACIS 2015 Session (SS4): Verified Numerical Computations
Aim and Scope
This special session is devoted to verified numerical computations related to self-validating methods and computer-assisted proofs. The verified numerical computations play important roles for rigorously solving linear and nonlinear equations. The main objective of the session is to discuss several recent topics on the verified numerical computations and numerical methods.
Topics (including, but not limited to)
- Computer-assisted proofs for ODE and PDE
- Verified numerical linear algebra
- Verified numerical computations for dynamical systems
- Mathematics for verified numerical computations
- Applications of verified numerical computations
- A short abstract will appear on the conference web page
as soon as accepted,
and in the post-conference proceedings to be
published by Springer LNCS.
- A journal special issue consisting of full papers
will be organized for consideration
in the journal
Mathematics in Computer Science,
- If you would like to give a talk at MACIS, you need to submit
at least a SHORT paper -- see
for the details.
- The deadline for all submissions is
August 11, 2015 September 1, 2015 -- see the Call for Papers for the details
- After the meeting,
the submission guideline for a journal special issue
will be communicated to you by the session organizers.
Nobito Yamamoto (The University of Electro-Communications, Japan), Kaname Matsue (Institute of Statistical Mathematics, Japan), Tomohiro Hiwaki (The University of Electro-Communications, Japan)
We provide a systematic method to validate the domain of Lyapunov functions around hyperbolic fixed points both for continuous and for discrete dynamical systems with computer assistance.
We also give the construction of Lyapunov functions around periodic orbits as fixed points of Poincaré maps as well as validation examples in our talk.
Kenta Kobayashi (Hitotsubashi University, Japan)
We present a recursive formula which gives the circumradius of the n-simplex in terms of the circumradius of its facets. Our formula shows that the circumradius of the n-simplex is closely related to the distances from each vertex to the circumcenter of the opposite facet. In particular, our formula shows that the circumradius of the tetrahedron can be expressed by the areas of the pedal triangles of each facet. We could only prove the formula for n up to 5, but numerical results strongly suggest that our formula holds true for any n.
Takehiko Kinoshita (Kyoto University), Yoshitaka Watanabe (Kyushu University), Mitsuhiro Nakao (National Institute of Technology, Sasebo College)
This paper presents two equalities of H3 and H4 semi-norms for the solutions of the Poisson equation in a two-dimensional polygonal domain. These equalities enable us to obtain higher order constructive a priori error estimates for finite element approximation of the Poisson equation with validated computing.
Katsuhisa Ozaki (Shibaura Institute of Technology), Takeshi Ogita (Tokyo Woman's Christian University)
This paper is concerned with accurate computations for matrix multiplication.
An error-free transformation of matrix multiplication is developed by authors.
It transforms a product of two floating-point matrices to a sum of several floating-point matrices by using only floating-point arithmetic. This transformation is useful for not only accurate computations for matrix multiplication but also interval enclosure of matrix multiplication. The key technique is an error-free splitting of floating-point numbers. We improve the error-free splitting and develop a posteriori validation method for the error-free transformation.
Akitoshi Takayasu (Waseda University), Makoto Mizuguchi (Waseda University), Takayuki Kubo (University of Tsukuba), Shin'Ichi Oishi (Waseda University)
This article presents a theorem for guaranteeing existence of a solution for an initial-boundary value problem of semilinear parabolic equations. The sufficient condition of our main theorem is derived by a fixed-point formulation using the evolution operator. We note that the sufficient condition can be checked by verified numerical computations.
Naoya Yamanaka (Teikyo Heisei University), Tomoaki Okayama (Hiroshima City University), Shin'Ichi Oishi (Waseda University)
An algorithm is presented for computing verified error bounds for the value of the real gamma function. It has been shown that the double exponential formula is one of the most efficient methods for calculating integrals of the form. Recently, an useful evaluation based on the double exponential formula over the semi-infinite interval has been proposed. However, the evaluation would be overflow when applied to the real gamma function directly. In this paper, we present a theorem so as to overcome the problem in such a case. Numerical results are presented for illustrating effectiveness of the proposed theorem in terms of the accuracy of the calculation.