Computer algebra and theorem proving: a pragmatic approach

We report informally on our experiences in working with NAG Ltd, developers of the AXIOM compuer algebra system, to find ways in which theorem proving could help users of computer algebra systems. The first project involves development of an annotation language and a VC generator for the AXIOM/Aldor system. The second is the use of theorem proving support to help with a specific problem computer algebra systems are not very good at: evaluating symbolic definite integrals.

LS Home page or Talks in 1998/99