{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404211,"version":"3.41.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2001,11]]},"DOI":"10.1023\/a:1011908113514","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T11:29:09Z","timestamp":1040642949000},"page":"323-351","source":"Crossref","is-referenced-by-count":28,"title":["Nonstandard Analysis in ACL2"],"prefix":"10.1007","volume":"27","author":[{"given":"Ruben A.","family":"Gamboa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"338921_CR1","first-page":"353","volume":"24","author":"A. Ballantyne","year":"1997","unstructured":"Ballantyne, A. and Bledsoe, W. W.: Automatic proofs of theorems in analysis using nonstandard techniques, J. Assoc. Comput. Mach. (JACM)\n24(3) (1997), 353\u2013371.","journal-title":"J. Assoc. Comput. Mach. (JACM)"},{"key":"338921_CR2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-94-011-3488-0_3","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"A. M. Ballantyne","year":"1991","unstructured":"Ballantyne, A. M.: The metatheorist: Automatic proofs of theorems in analysis using nonstandard techniques, Part II, in R. S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, Dordrecht, 1991, pp. 61\u201375."},{"key":"338921_CR3","series-title":"Technical Report","volume-title":"The UT natural deduction prover","author":"W. W. Bledsoe","year":"1983","unstructured":"Bledsoe, W. W.: The UT natural deduction prover, Technical Report ATP-17B, University of Texas at Austin, 1983."},{"key":"338921_CR4","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W.: Some automatic proofs in analysis, Contemp. Math.\n29 (1984).","DOI":"10.1090\/conm\/029\/06"},{"key":"338921_CR5","doi-asserted-by":"crossref","unstructured":"Boyer, R. S., Goldschlag, D., Kaufmann, M., and Moore, J S.: Functional instantiation in first order logic, in V. Lifschitz (ed.), Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, 1991, pp. 7\u201326.","DOI":"10.1016\/B978-0-12-450010-5.50007-4"},{"key":"338921_CR6","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, Orlando, 1979."},{"key":"338921_CR7","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S. and Moore, J S.:A Computational Logic Handbook, Academic Press, San Diego, 1988."},{"key":"338921_CR8","doi-asserted-by":"crossref","unstructured":"Brock, B.,Kaufmann, M., and Moore, J S.: ACL2 theorems about commercial microprocessors, in M. Srivas and A. Camilleri (eds.), Formal Methods in Computer-Aided Design (FMCAD '96), 1996, pp. 275\u2013293.","DOI":"10.1007\/BFb0031816"},{"key":"338921_CR9","doi-asserted-by":"crossref","unstructured":"Diener, F. and Diener, M. (eds.): Nonstandard Analysis in Practice, Springer, 1995.","DOI":"10.1007\/978-3-642-57758-1"},{"key":"338921_CR10","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS, in Proceedings of the Ninth International Conference on Theorem Proving in Higher-Order Logics (TPHOL '96), 1996.","DOI":"10.1007\/BFb0105402"},{"issue":"2","key":"338921_CR11","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"Farmer, W. M., Guttman, J. D., and Thayer, F. J.: IMPS: An interactive mathematical proof system, J. Automated Reasoning\n11(2) (1993), 213\u2013248.","journal-title":"J. Automated Reasoning"},{"key":"338921_CR12","unstructured":"Fleuriot, J.: A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton's Principia, Ph.D. Thesis, University of Cambridge, 1999."},{"key":"338921_CR13","series-title":"Technical Report","volume-title":"Square roots in ACL2: A study in sonata form","author":"R. Gamboa","year":"1996","unstructured":"Gamboa, R.: Square roots in ACL2: A study in sonata form, Technical Report CS-TR-96-34, University of Texas at Austin, 1996."},{"key":"338921_CR14","doi-asserted-by":"crossref","unstructured":"Gamboa, R.: Mechanically verifying the correctness of the fast Fourier transform in ACL2, in J. Rolim (ed.), Parallel and Distributed Processing, 1998, pp. 796\u2013806.","DOI":"10.1007\/3-540-64359-1_743"},{"key":"338921_CR15","volume-title":"Mechanically Verifying Real-Valued Algorithms in ACL2","author":"R. Gamboa","year":"1999","unstructured":"Gamboa, R.: Mechanically Verifying Real-Valued Algorithms in ACL2, Ph.D. Thesis, The University of Texas at Austin, 1999."},{"key":"338921_CR16","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"R. Gamboa","year":"2000","unstructured":"Gamboa, R.: Continuity and differentiability in ACL2, in M. Kaufmann, P. Manolios and J S. Moore (eds.), Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Dordrecht, 2000, Chapt. 18."},{"key":"338921_CR17","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers, Ph.D. Thesis, University of Cambridge, 1996."},{"key":"338921_CR18","unstructured":"Jr., G. L. S.: Common LISP The Language, 2nd edn, Digital Press, Bedford, MA, 1990."},{"key":"338921_CR19","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M.: Modular proof: The fundamental theorem of calculus, in M. Kaufmann, P. Manolios and J S. Moore (eds.), Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, Dordrecht, 2000, Chapt. 6."},{"key":"338921_CR20","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., and Moore, J S.: Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Dordrecht, 2000."},{"key":"338921_CR21","unstructured":"Kaufmann, M. and Moore, J S.: ACL2: A computational logic for applicative common lisp, the user's manual. Available on theWorld-WideWeb at http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/acl2-doc.html."},{"key":"338921_CR22","unstructured":"Kaufmann, M. and Moore, J S.: A precise description of the ACL2 logic, Available on the World-Wide Web at http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/km97a.ps. Z."},{"key":"338921_CR23","unstructured":"Kaufmann, M. and Moore, J S.: Design goals for ACL2, Technical Report 101, Computational Logic, Inc., 1994. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/-acl2-paper s.html#Overviews."},{"issue":"1","key":"338921_CR24","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M. and Moore, J S.: Structured theory development for a mechanized logic, J. Automated Reasoning\n26(1) (2001), 161\u2013203.","journal-title":"J. Automated Reasoning"},{"key":"338921_CR25","volume-title":"Elementary Calculus, Prindle","author":"H. J. Keisler","year":"1976","unstructured":"Keisler, H. J.: Elementary Calculus, Prindle, Weber and Schmidt, Boston, 1976."},{"issue":"9","key":"338921_CR26","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J. S. Moore","year":"1998","unstructured":"Moore, J S., Lynch, T., and Kaufmann, M.: A mechanically checked proof of the AMD5K86 floating-point division program, IEEE Trans. Comp.\n47(9) (1998), 913\u2013926.","journal-title":"IEEE Trans. Comp."},{"key":"338921_CR27","unstructured":"Nelson, E.: On-line books: Internal set theory, Available on the World-Wide Web at http:\/\/www.math.princeton.edu\/nelson\/books.html."},{"key":"338921_CR28","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1090\/S0002-9904-1977-14398-X","volume":"83","author":"E. Nelson","year":"1977","unstructured":"Nelson, E.: Internal set theory, Bull. Amer. Math. Soc.\n83 (1977), 1165\u20131198.","journal-title":"Bull. Amer. Math. Soc."},{"key":"338921_CR29","doi-asserted-by":"crossref","unstructured":"Owre, S., Rajan, S., Rushby, J. M., Shankar, N., and Srivas, M. K.: PVS: Combining specification, proof checking, and model checking, in R. Alur and T. A. Henzinger (eds.), Computer-Aided Verification, CAV '96, Lecture Notes in Comput. Sci. 1102, New Brunswick, NJ, 1996, pp. 411\u2013414.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"338921_CR30","unstructured":"Robert, A.: Non-Standard Analysis, Wiley, 1988."},{"key":"338921_CR31","doi-asserted-by":"crossref","unstructured":"Robinson, A.: Non-Standard Analysis, Princeton University Press, 1996.","DOI":"10.1515\/9781400884223"},{"key":"338921_CR32","unstructured":"Rudnicki, P.: An overview of the MIZAR project, in Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992."},{"key":"338921_CR33","first-page":"148","volume":"1","author":"D. Russinoff","year":"1998","unstructured":"Russinoff, D.: A mechanically checked proof of IEEE compliance of a register-transferlevel specification of the AMD-K7 floating-point multiplication, division, and square root instructions, London Math. Soc. J. Comput. Math.\n1 (1998), 148\u2013200.","journal-title":"London Math. Soc. J. Comput. Math."},{"key":"338921_CR34","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D. Russinoff","year":"1999","unstructured":"Russinoff, D.: A mechanically checked proof of correctness of the AMD-K5 floating-point square root microcode, Formal Methods in System Design\n14 (1999), 75\u2013125.","journal-title":"Formal Methods in System Design"},{"key":"338921_CR35","unstructured":"Trybulec, A.: The Mizar-QC\/6000 logic information language, Bull. Assoc. Literary and Linguistic Computing (LLAC)\n6(2) (1978)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011908113514.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011908113514\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011908113514.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:34:47Z","timestamp":1749123287000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011908113514"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2001,11]]}},"alternative-id":["338921"],"URL":"https:\/\/doi.org\/10.1023\/a:1011908113514","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}