Ursula Martin

Computational math: the new challenge for computational logic

Scientific computation based on continuous computational mathematics is widely used for applications as diverse as high energy physics, weather forecasting, environmental and financial modelling, and is becoming important in systems design for engineering applications like air-traffic control algorithms or synthesising code for control systems. Complex models and simulations are among the most demanding of computer power. The leading commercial software systems such as Maple 6, MATLAB and NAG have around 2 million users, and scientists and engineers have in-house code for many specialised applications. Computational mathematics systems may be numeric or symbolic: both can be subject to error and problems of scale, and lack a framework for reasoning about the models they implement. Computational logic systems allow such reasoning, and do the underlying mathematics analytically, so we can rely on the answers they produce.

We give an overview of recent work at St Andrews and elsewhere in applying computational logic to computational mathematics, and set out some challenges:

for its immediate application as an effective component of mathematical software such as Maple or for representing mathematical knowledge as part of endeavours like OpenMath/MathML

for the use of computational logic techniques to support applied math and mathematical modeling, particularly in areas where the highest degree of assurance is required, such as avionics

for developing a strategy for the representation, validation and communication of mathematics and science in a future where the opportunities and challenges of digitally embodied knowledge may radically change scholarship and scientific discourse