Verification Methods and Symbolic Computations

Our intpakX package extends the computer algebra system Maple.It allows, e.g., veried numerical calculations (computer-assisted proofs) builton arbitrary precision interval operations. Up to now, only the basic operationsare supported in a guaranteed way. Concerning higher mathematicalfunctions supported in Maple, there are no data about their accuracies available/published. Thus, it is not possible or at least very hard to build arbitraryprecision interval functions using Maple's intrinsic mathematical functions(nevertheless, intpakX oers such function implementations using someguard digits in an experimental way, which - of course - is not really a reliablemathematical approach).On the other hand there are software packages supporting reliable multipleprecision 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 indetail. We emphasize the dierent approaches (arbitrary precision arithmetic,staggered correction arithmetic, functions only for real arguments, functionsfor complex arguments, ...) and the most important resulting properties of thecorresponding implementations. We also compare their performance and wecomment on the actual integration of several of these libraries in C-XSC. Themissing step is to bring together C-XSC and computer algebra packages likeMaple and Mathematica. Combining fast verication methods and symboliccomputations deeply extends the range of applications of rigorous mathematicalmethods.