Dependable Computer Algebra
Speaker: Andrew Adam
Time: Wednesday 21st June 2000, at 15.15
Place: Room 2.33
Abstract:
Mathematics on computers has diverged into a number of different areas:
Theorem Proving (logic), Computer Algebra (computational algebra).
Numerical Analysis (floating point computation) and Exact Real Computation
(continued fractions). I will talk about Computer Algebra Systems and their
problems, and how we have used Theorem Proving to show ways of overcoming
these problems.
Computer Algebra Systems almost invariably began life as a set of individual
routines for specific calculations in computational algebra: computing
the generators of a permutation group or the grobner basis of an ideal.
As they developed more work was put into general interfaces and genetralising
the routines to more and more areas of computational algebra and related
fields. The culmination of this was the general mathematical assistant
such as Maple (tm) or Mathematica (tm). Their basis as a collection
of routines for computational algebra still remains however ans computer
algebra systems remain good at calculating algebraic answers but
poor at dealing with logical side conditions.
As a case study to assess whether trheorem proving can be used to provide
logical support for computer algebra calculation, we have considered the
problems of definite integration. As part of a proposed solution to some
of the problems of calculating define integrals we have produced a look
up table for definite integrals involving parameters, which uses a library
for real number theorem proving in PVS to discharge side conditions. I
will explain the issues involved in building such a system in terms of
analysis of the analytical problem and the automatic theorem proving issues.