Overview: Integrating computer algebra and reasoning

Project overview

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,

a system might need to assume that a variable x is non-zero when dividing by x, but not make that assumption explicit;
a system might use a naive algorithm to perform integration which ignores potential singularities.

An experienced user will be able to keep track of these issues in a small example, but in the large the problem is much more difficult. Because of this, there has been considerable interest in combining symbolic mathematics with formal logic reasoning, and indeed a number of the different possible ways in which CA systems and theorem provers can be interconnected have already been proposed.

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.