**Next:**Conditions on Transformations.

**Up:**The Explanation Problem

**Previous:**Access to Libraries

## Value of Precise Mathematical Language

The three examples of the explanation problem discussed above all arose in our work. They are representative of problems that have faced applied mathematicians and engineers for years. One solution pursued by the scientific community has been to be more precise and careful. The algorithm's pre-conditions are specified carefully, e.g., the fact that must be nonzero for QuadIntegral:Eq to be valid. Theorems that characterize the applicability of an algorithm, for example that a particular meshing algorithm is only valid for piecewise smooth 2-manifolds. And finally, reference books have been developed that precisely document the standard library algorithms in terms of the communal database of mathematical knowledge [61,48,49] . Indeed it is the elaborate knowledge base that characterizes the domain in which we work.

The emergence of applied logic and formal methods has opened new opportunities for computers to help in more effectively employing the methodology of mathematics. We now know how to specify algorithms rigorously and how to create semi-formal databases. We look at how two specific examples are treated.

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995