Computer-Assisted Proofs and Symbolic Computations

Krämer, Walter. "Computer-Assisted Proofs and Symbolic Computations." Serdica Journal of Computing 4.1 (2010): 73-84. <http://eudml.org/doc/11376>.

@article{Krämer2010,
abstract = {We discuss some main points of computer-assisted proofs based on reliable numerical computations. Such so-called self-validating numerical methods in combination with exact symbolic manipulations result in very powerful mathematical software tools. These tools allow proving mathematical statements (existence of a fixed point, of a solution of an ODE, of a zero of a continuous function, of a global minimum within a given range, etc.) using a digital computer. To validate the assertions of the underlying theorems fast finite precision arithmetic is used. The results are absolutely rigorous. To demonstrate the power of reliable symbolic-numeric computations we investigate in some details the verification of very long periodic orbits of chaotic dynamical systems. The verification is done directly in Maple, e.g. using the Maple Power Tool intpakX or, more efficiently, using the C++ class library C-XSC.* This work is partially supported by DFG: KR1612/7-1.},
author = {Krämer, Walter},
journal = {Serdica Journal of Computing},
keywords = {Computer-Assisted Proofs; Symbolic Computations; Self-Validating Numerical Methods; Dynamical System; Verified Periodic Orbit; IntpakX; C-XSC; computer-assisted proofs; symbolic computation; self-validating numerical methods; dynamical system; verified periodic orbit; intpakX; C-XSC; mathematical software},
language = {eng},
number = {1},
pages = {73-84},
publisher = {Institute of Mathematics and Informatics Bulgarian Academy of Sciences},
title = {Computer-Assisted Proofs and Symbolic Computations},
url = {http://eudml.org/doc/11376},
volume = {4},
year = {2010},
}

TY - JOUR
AU - Krämer, Walter
TI - Computer-Assisted Proofs and Symbolic Computations
JO - Serdica Journal of Computing
PY - 2010
PB - Institute of Mathematics and Informatics Bulgarian Academy of Sciences
VL - 4
IS - 1
SP - 73
EP - 84
AB - We discuss some main points of computer-assisted proofs based on reliable numerical computations. Such so-called self-validating numerical methods in combination with exact symbolic manipulations result in very powerful mathematical software tools. These tools allow proving mathematical statements (existence of a fixed point, of a solution of an ODE, of a zero of a continuous function, of a global minimum within a given range, etc.) using a digital computer. To validate the assertions of the underlying theorems fast finite precision arithmetic is used. The results are absolutely rigorous. To demonstrate the power of reliable symbolic-numeric computations we investigate in some details the verification of very long periodic orbits of chaotic dynamical systems. The verification is done directly in Maple, e.g. using the Maple Power Tool intpakX or, more efficiently, using the C++ class library C-XSC.* This work is partially supported by DFG: KR1612/7-1.
LA - eng
KW - Computer-Assisted Proofs; Symbolic Computations; Self-Validating Numerical Methods; Dynamical System; Verified Periodic Orbit; IntpakX; C-XSC; computer-assisted proofs; symbolic computation; self-validating numerical methods; dynamical system; verified periodic orbit; intpakX; C-XSC; mathematical software
UR - http://eudml.org/doc/11376
ER -