References about automatic result verification

[George Corliss]

Jeff Dawson (dawsonardvax.enet.dec.com) writes:
> I saw your recent contribution to numeric-interest regarding interval 
> arithmetic. I was particularly curious about automatic result verification
> and wondered if you might be able to point me to some references.

Sure.  Here are several good references:

Ray Moore,
Interval Analysis,
Prentice-Hall, 1996.

  The classic in the field.  Now out of print.

Ray Moore,
Methods and Applications of Interval Analysis,
SIAM, Philadelphia, 1979.  ISBN: 0-89871-161-4.

  Very readable introduction to intervals.  Contains at least the kernel 
  of the ideas of nearly all interval algorithms.  800+ entry bibliography
  of the first two decages of interval studies.

G. Alefeld and J. Herzberger,
Introduction to Interval Computations,
Academic Press, Orlando, 1983.  ISBN: 0-12-049820-0.

  Good introduction.  More detailed than Moore's.  Covers real and complex
  interval arithmetic and their machine realization.  Addresses many
  problem areas from linear and nonlinear systems.  500+ entry bibliography.

H. Ratschek and J. Rokne,
Computer Methods for the Range of Functions,
Halsted Press, New York, 1984.

  Bounding the range of a function is THE fundamental problem in interval
  computations.  This is how it can be done, with all its variants.

Arnold Neumaier,
Interval Methods for Systems of Equations,
Cambridge, 1990.  ISBN: 0-521-33196-X

  Mathematically very careful and rigorous.  Builds the tools from
  precise theory.  Surveys the basic properties of interval arithmetic
  and enclosing the range of a function.  Algorithms for square linear
  and for nonlinear systems of equations.  Exceptionally complete
  bibliography for further study.  If you intend to program interval
  algorithms, this is a MUST READ to minimize wheel re-invention.

Eldon Hansen,
Global Optimization Using Interval Analysis,
Dekker, New York, 1992.  ISBN: 0-8247-8696-3

   Very readable.  Gives a quick survey of interval techniques.
   Covers selected methods for linear equations and inequalities.
   Then gives detailed algorithms for interval Newton, unconstrained
   and several types of constrained optimization.  Yet another
   extensive bibliography.

There are many other references for interval computations I could give,
but this should get you started.

"Automatic Result Verification or Validation" includes, but is not limited
to, interval techniques.  The intention is that the computer should be 
able to make a mathematical assertion about something (such as, "There
exists a unique solution contained in the interval [a, b]"), usually by
verifying the hypotheses of some appropriate mathematical theorem. 
Besides interval techniques, symbolic techniques or theorem-proving
may be used.  I know of no survey book on automatic result verification,
so I will point you instead to several collections of papers.

U. Kulisch and H.J. Stetter (editors),
Scientific Computation with Automatic Result Verification,
Computing Supplementum 6,
Springer-Verlag, New York, 1988.

  Includes good introductory article by Kulisch and Stetter defining
  "automatic result verification."  Articles cover methods, applications,
  and tools.

Kenneth Meyer and Dieter Schmidt (editors),
Computer Aided Proofs in Analysis,
Springer-Verlag IMA Volume in Mathematics and Its Applications # 28, 1991.
ISBN: 0-387-97426-1.

  Similar questions, slightly different perspective.

Christian Ullrich (editor),
Computer Arithmetic and Self-Validating Numerical Methods,
Academic Press Notes and Reports in Mathematics in Science
  and Engineering Volume 7, 1990.  ISBN: 0-12-708245-X.

  Proceedings of an international conference held in Basel, October 1989.

Ernst Adams and Ulrich Kulisch (editors),
Scientific Computating with Automatic Result Verification,
just appeared.  I don't know the publisher, but Springer is likely.

  Collection of articles from Karlsruhe on methods, tools, and applications
  of self-validating methods.


That should be enough for this week :-)  Then follow the references in
any of the works cited here.

George F. Corliss
Department of Mathematics
Marquette University
Milwaukee, WI  53233  USA
georgecaboris.mscs.mu.edu