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.