A Deductive Database for Mathematical formulas

Stéphane Dalmas, Marc Gaëtano, Claude Huchet

Date: July 17th (Wednesday)
Time: ??.??
Abstract
In this talk, we present mfd2, a deductive database for mathematical formulas. Mathematical relations such as the ones defined in the Handbook of mathematical functions (by M. Abramovitz and I. Stegun) can be stored in and retrieved from mfd2.
The database itself is a stand-alone program which can run as a client in a client/server environment and it has been designed to be a powerful assistant for computer algebra systems as well as for other applications. For example, mfd2 could be the heart of an electronic handbook of mathematical relations or could be used as a lemma database for a theorem prover. The information stored in mfd2 is accessed through a specialized query language.
A formula is always associated with its conditions of validity. These conditions are central to the retrieval mechanism of the database: mfd2 usually answers to a query conditionaly. For example, if we ask the simple query ex > 0 for x complex ? mfd2 would not just answer false but it would answer true if x is real''.
At the heart of mfd2 is a deduction engine based on an algorithm for associate-commutative unification that takes care of the conditions associated with the formulas. To solve a particular query, the engine first tries to find a ``close enough'' formula in the database using associate-commutative unification. If it fails, the engine tries to analyse the failure reasons to generate some equations that can make the formula and the query to match. It then tries to solve these new equations using the statements contained in the database and some built-in mathematical transformations. This can produce some new conditions (conditions for some solution to hold) that are in turn analyzed by calling the database recursively. The complexity of this process is controlled by carefully chosing an order on the formulas in the database, depending on the query.

______________
__________________________________________

Previous page RISC SWP Linz Austria