References

  1. A.M. Ballantyne & W. W. Bledsoe (1977): Automatic Proofs of Theorems in Analysis Using Non-Standard Techniques. Journal of the Association for Computing Machinery (JACM) 24(3), pp. 353–371, doi:10.1145/322017.322018.
  2. R. Gamboa (1999): Mechanically Verifying Real-Valued Algorithms in ACL2. The University of Texas at Austin.
  3. R. Gamboa & J. Cowles (2007): Theory Extension in ACL2(r). Journal of Automated Reasoning, doi:10.1007/s10817-006-9043-0.
  4. M. Kaufmann (2000): Modular Proof: The Fundamental Theorem of Calculus. In: M. Kaufmann, P. Manolios & J S. Moore: Computer-Aided Reasoning: ACL2 Case Studies, chapter 6. Kluwer Academic Press, doi:10.1007/978-1-4615-4449-4.
  5. E. Nelson (1977): Internal Set Theory: A New Approach to Nonstandard Analysis. Bulletin of the American Mathematical Society 83, pp. 1165–1198, doi:10.1090/S0002-9904-1977-14398-X.
  6. P. Reid & R. Gamboa (2011): Automatic Differentiation in ACL2. In: Proc of the Second Conference on Interactive Theorem Proving (ITP-2011), doi:10.1007/978-3-642-22863-6_23.
  7. A. Robinson (1996): Non-Standard Analysis. Princeton University Press.
  8. W. Rudin (1976): Principles of Mathematical Analysis, third edition. McGraw-Hill.
  9. J. Sawada & R. Gamboa (2002): Mechanical Verification of a Square Root Algorithm using Taylor's Theorem. In: Formal Methods in Computer-Aided Design (FMCAD'02), doi:10.1007/3-540-36126-X_17.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org