Computer-Assisted Proofs and Symbolic Computations
Walter Kraemer
Last modified: 2010-03-31
Abstract
Our intpakX package extends the computer algebra system Maple. It allows, e.g.,
verified numerical calculations (computer-assisted proofs) built on arbitrary
precision interval operations.
Up to now, only the basic operations are supported in a guaranteed way.
Concerning higher mathematical functions supported in Maple, there are
no data about their accuracies available/published. Thus, it is not possible or at
least very hard to build arbitrary precision interval functions using Maple's
intrinsic mathematical functions (nevertheless intpakX offers such function implementations
using some guard digits in an experimental way, which - of course - is not
really a reliable mathematical approach).
On the other hand there are software packages supporting reliable multiple precision
interval functions like C-XSC, the MPFR and the MPFI libraries, and others.
In the talk we discuss the features of some of these libraries in detail.
We emphasize the
different approaches (arbitrary precision arithmetic, staggered correction
arithmetic, functions only for real arguments, functions for complex arguments,
...) and the most important resulting properties of the corresponding implementations.
We also compare their performance and
we comment on the actual integration of several of these libraries in C-XSC.
The missing step is to bring together C-XSC and computer algebra packages
like Maple and Mathematica. For a first approach using communication protocols
see the talk 'Embedding C-XSC Automatic Differentiation in Mathematica'
of Evgenija Popova.
The International Association of Applied Mathematics and Mechanics (GAMM)
has founded the GAMM Activity Group "Computer-Assisted Proofs and Symbolic Computations"
in 2008.
verified numerical calculations (computer-assisted proofs) built on arbitrary
precision interval operations.
Up to now, only the basic operations are supported in a guaranteed way.
Concerning higher mathematical functions supported in Maple, there are
no data about their accuracies available/published. Thus, it is not possible or at
least very hard to build arbitrary precision interval functions using Maple's
intrinsic mathematical functions (nevertheless intpakX offers such function implementations
using some guard digits in an experimental way, which - of course - is not
really a reliable mathematical approach).
On the other hand there are software packages supporting reliable multiple precision
interval functions like C-XSC, the MPFR and the MPFI libraries, and others.
In the talk we discuss the features of some of these libraries in detail.
We emphasize the
different approaches (arbitrary precision arithmetic, staggered correction
arithmetic, functions only for real arguments, functions for complex arguments,
...) and the most important resulting properties of the corresponding implementations.
We also compare their performance and
we comment on the actual integration of several of these libraries in C-XSC.
The missing step is to bring together C-XSC and computer algebra packages
like Maple and Mathematica. For a first approach using communication protocols
see the talk 'Embedding C-XSC Automatic Differentiation in Mathematica'
of Evgenija Popova.
The International Association of Applied Mathematics and Mechanics (GAMM)
has founded the GAMM Activity Group "Computer-Assisted Proofs and Symbolic Computations"
in 2008.