Richard J. Fateman. High-level proofs of mathematical programs using automatic differentiation, simplification, and some common sense. In J. Rafael Sendra, editor, Symbolic and Algebraic Computation, International Symposium ISSAC 2003, Drexel University, Philadelphia, Pennsylvania, USA, August 3-6, 2003, Proceedings. pages 88-94, ACM, 2003. [doi]
Abstract is missing.