Symbolic mathematical - or computer algebra (CA) - systems, such as Axiom, Maple and Mathematica, are in everyday use by scientists, engineers and indeed mathematicians, because they provide a user with techniques of, say, integration which far exceed those of the person themselves, and make routine many calculations which would have been impossible some years ago. These systems are, moreover, taught as standard tools within many university undergraduate programmes and are used in support of both academic and commercial research.
There are, however, drawbacks to the widespread use of automated support of complex mathematical tasks, which have been widely noted. For example,
Our project is to explore the integration of reasoning capabilities into the Axiom system, or more specifically into the Axiom library compiler, Aldor, and to use this integrated logic to improve support for symbolic mathematics. The integration will make the practice of symbolic mathematics more reliable - by incorporating conditions on the application of certain operations, for instance. It will also extend what it is possible to achieve with CA by allowing logical reasoning as a part of symbolic computation.
In order to focus the project on needs of users of symbolic mathematics -
rather than the ideas of system developers -
an integral part of the project is a mathematical case study in symbolic
asymptotics.
This is a topic where we
anticipate that a logical approach will have benefits. For instance, in
exploring the
asymptotic behaviour of functions like exp(k*x^2)
it crucial
to know the sign of constant terms, such as k
. From a logical point of
view we can represent this situation by adding the appropriate pre-conditions
to various operations; these pre-conditions can then be proved
when the operations are applied (or can serve as explicit documentary warnings
in the form of proof
obligations, if we adopt a `lightweight' approach).
The approach which we propose for integrating CA and reasoning is novel. Aldor is distinctive among CA systems in having an advanced type theory-- including `dependent' types. Our principal aim in the project is to use a modified version of the types of Aldor itself directly to represent a logic and thus directly to support a reasoning capacity within the Axiom system itself. This has the benefit of not requiring there to be two systems within which to operate - one computer algebra system and one reasoning system - and allows axiomatised theories to be built in exactly the same way that Aldor categories are currently built. The logic we build will be a version of the logic used in a number of existing theorem provers, such as Coq.