Theory Extension in ACL2(r)

1. Boyer, R.S., Goldschlag, D., Kaufmann, M., Moore, J.S.: Functional instantiation in first order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7–26 (1991)

2. Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, Orlando (1979)

   MATH  Google Scholar 

3. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic, San Diego (1988)

   MATH  Google Scholar 

4. Diener, F., Diener, M. (eds.): Nonstandard Analysis in Practice. Springer, Berlin Heidelberg New York (1995)

   MATH  Google Scholar 

5. Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason. 27(4), 323–351 (2001)

   Article  MATH  MathSciNet  Google Scholar 

6. Gamboa, R., Middleton, B.: Taylor’s formula with remainder. In: Proc of the Third International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2002), 2002

7. Kanovei, V., Reeken, M.: Nonstandard Analysis, Axiomatically. Springer, Berlin Heidelberg New York (2004)

   MATH  Google Scholar 

8. Kaufmann, M.: Modular proof: the fundamental theorem of calculus. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Chapt. 6. Kluwer, Norwell, Massachusetts (2000)

   Google Scholar 

9. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Norwell, Massachusetts (2000)

   Google Scholar 

10. Kaufmann, M., Moore, J.S.: ACL2 Documentation topic on conservativity of defchoose. Available in the ACL2 distribution since version 2.9.2 with :DOC CONSERVATIVITY-OF-DEFCHOOSE

11. Kaufmann, M., Moore, J.S.: A precise description of the ACL2 logic. http://www.cs.utexas.edu/users/moore/publications/km97a.ps.Z

12. Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161–203 (2001)

    Article  MATH  MathSciNet  Google Scholar 

13. Gameiro, M., Manolios, P.: Formally verifying an algorithm based on interval arithmetic for checking transversality. In: Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004), 2004

14. Nelson, E.: On-line books: internal set theory. Available on the world-wide web at http://www.math.princeton.edu/ñelson/books.html

15. Nelson, E.: Internal set theory: a new approach to nonstandard analysis. Bull. Am. Math. Soc. 83, 1165–1198 (1977)

    Article  MATH  Google Scholar 

16. Robert, A.: Non-Standard Analysis. Wiley, New York (1988)

    Google Scholar 

17. Robinson, A.: Non-Standard Analysis. Princeton University Press, Princeton, New Jersey (1996)

    MATH  Google Scholar 

18. Sawada, J., Gamboa, R.: Mechanical verification of a square root algorithm using Taylor’s theorem. In: Formal Methods in Computer-Aided Design (FMCAD’02), 2002

Download references